Fintype instances for pi types #
def
Fintype.piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
(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
- Fintype.piFinset t = Finset.map { toFun := fun (f : (a : α) → a ∈ Finset.univ → δ a) (a : α) => f a ⋯, inj' := ⋯ } (Finset.pi Finset.univ t)
Instances For
@[simp]
theorem
Fintype.mem_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
{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_3}
(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_3}
(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_3}
[Nonempty α]
:
(Fintype.piFinset fun (x : α) => ∅) = ∅
@[simp]
theorem
Fintype.piFinset_nonempty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_2}
{s : (a : α) → Finset (γ a)}
:
(Fintype.piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty
@[simp]
theorem
Fintype.piFinset_of_isEmpty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_2}
[IsEmpty α]
(s : (a : α) → Finset (γ a))
:
Fintype.piFinset s = Finset.univ
@[simp]
theorem
Fintype.piFinset_singleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
(f : (i : α) → δ i)
:
(Fintype.piFinset fun (i : α) => {f i}) = {f}
theorem
Fintype.piFinset_subsingleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
{f : (i : α) → Finset (δ i)}
(hf : ∀ (i : α), Set.Subsingleton ↑(f i))
:
theorem
Fintype.piFinset_disjoint_of_disjoint
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
(t₁ : (a : α) → Finset (δ a))
(t₂ : (a : α) → Finset (δ a))
{a : α}
(h : Disjoint (t₁ a) (t₂ a))
:
Disjoint (Fintype.piFinset t₁) (Fintype.piFinset t₂)
theorem
Fintype.piFinset_image
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_2}
{δ : α → Type u_3}
[(a : α) → DecidableEq (δ a)]
(f : (a : α) → γ a → δ a)
(s : (a : α) → Finset (γ a))
:
(Fintype.piFinset fun (a : α) => Finset.image (f a) (s a)) = Finset.image (fun (b : (a : α) → γ a) (a : α) => f a (b a)) (Fintype.piFinset s)
theorem
Fintype.eval_image_piFinset_subset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
(t : (a : α) → Finset (δ a))
(a : α)
[DecidableEq (δ a)]
:
Finset.image (fun (f : (a : α) → δ a) => f a) (Fintype.piFinset t) ⊆ t a
theorem
Fintype.eval_image_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
(t : (a : α) → Finset (δ a))
(a : α)
[DecidableEq (δ a)]
(ht : ∀ (b : α), a ≠ b → (t b).Nonempty)
:
Finset.image (fun (f : (a : α) → δ a) => f a) (Fintype.piFinset t) = t a
theorem
Fintype.eval_image_piFinset_const
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{β : Type u_4}
[DecidableEq β]
(t : Finset β)
(a : α)
:
Finset.image (fun (f : α → β) => f a) (Fintype.piFinset fun (_i : α) => t) = t
theorem
Fintype.filter_piFinset_of_not_mem
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
[(a : α) → DecidableEq (δ a)]
(t : (a : α) → Finset (δ a))
(a : α)
(x : δ a)
(hx : x ∉ t a)
:
Finset.filter (fun (x_1 : (a : α) → δ a) => x_1 a = x) (Fintype.piFinset t) = ∅
theorem
Fintype.piFinset_update_eq_filter_piFinset_mem
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
[(a : α) → DecidableEq (δ a)]
(s : (i : α) → Finset (δ i))
(i : α)
{t : Finset (δ i)}
(hts : t ⊆ s i)
:
Fintype.piFinset (Function.update s i t) = Finset.filter (fun (f : (a : α) → δ a) => f i ∈ t) (Fintype.piFinset s)
theorem
Fintype.piFinset_update_singleton_eq_filter_piFinset_eq
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_3}
[(a : α) → DecidableEq (δ a)]
(s : (i : α) → Finset (δ i))
(i : α)
{a : δ i}
(ha : a ∈ s i)
:
Fintype.piFinset (Function.update s i {a}) = Finset.filter (fun (f : (a : α) → δ a) => f i = a) (Fintype.piFinset s)
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 := ⋯ }
@[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)]
: