Fintype instances for pi types #
def
Fintype.piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
(t : (a : α) → Finset (δ a))
:
Finset ((a : α) → δ a)
Given for all a : α a finset t a of δ a, then one can define the
finset Fintype.piFinset t of all functions taking values in t a for all a. This is the
analogue of Finset.pi where the base finset is univ (but formally they are not the same, as
there is an additional condition i ∈ Finset.univ in the Finset.pi definition).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Fintype.mem_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
{t : (a : α) → Finset (δ a)}
{f : (a : α) → δ a}
:
f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a
@[simp]
theorem
Fintype.coe_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
(t : (a : α) → Finset (δ a))
:
↑(Fintype.piFinset t) = Set.pi Set.univ fun a => ↑(t a)
theorem
Fintype.piFinset_subset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
(t₁ : (a : α) → Finset (δ a))
(t₂ : (a : α) → Finset (δ a))
(h : ∀ (a : α), t₁ a ⊆ t₂ a)
:
@[simp]
theorem
Fintype.piFinset_empty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
[Nonempty α]
:
(Fintype.piFinset fun x => ∅) = ∅
@[simp]
theorem
Fintype.piFinset_singleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
(f : (i : α) → δ i)
:
(Fintype.piFinset fun i => {f i}) = {f}
theorem
Fintype.piFinset_subsingleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
{f : (i : α) → Finset (δ i)}
(hf : ∀ (i : α), Set.Subsingleton ↑(f i))
:
theorem
Fintype.piFinset_disjoint_of_disjoint
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_2}
(t₁ : (a : α) → Finset (δ a))
(t₂ : (a : α) → Finset (δ a))
{a : α}
(h : Disjoint (t₁ a) (t₂ a))
:
Disjoint (Fintype.piFinset t₁) (Fintype.piFinset t₂)
pi #
instance
Pi.fintype
{α : Type u_2}
{β : α → Type u_3}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
:
Fintype ((a : α) → β a)
A dependent product of fintypes, indexed by a fintype, is a fintype.
Equations
- Pi.fintype = { elems := Fintype.piFinset fun x => Finset.univ, complete := (_ : ∀ (a : (a : α) → β a), a ∈ Fintype.piFinset fun x => Finset.univ) }
@[simp]
theorem
Fintype.piFinset_univ
{α : Type u_2}
{β : α → Type u_3}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
:
(Fintype.piFinset fun a => Finset.univ) = Finset.univ
noncomputable instance
Function.Embedding.fintype
{α : Type u_2}
{β : Type u_3}
[Fintype α]
[Fintype β]
:
Equations
- Function.Embedding.fintype = Fintype.ofEquiv { f // Function.Injective f } (Equiv.subtypeInjectiveEquivEmbedding α β)
@[simp]
theorem
Finset.univ_pi_univ
{α : Type u_2}
{β : α → Type u_3}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
: