Documentation

Mathlib.Data.Fintype.Pi

Fintype instances for pi types #

def Fintype.piFinset {α : Type u_1} [inst : DecidableEq α] [inst : 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.
@[simp]
theorem Fintype.mem_piFinset {α : Type u_2} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_1} {t : (a : α) → Finset (δ a)} {f : (a : α) → δ a} :
f Fintype.piFinset t ∀ (a : α), f a t a
@[simp]
theorem Fintype.coe_piFinset {α : Type u_2} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_1} (t : (a : α) → Finset (δ a)) :
↑(Fintype.piFinset t) = Set.pi Set.univ fun a => ↑(t a)
theorem Fintype.piFinset_subset {α : Type u_2} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_1} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) (h : ∀ (a : α), t₁ a t₂ a) :
@[simp]
theorem Fintype.piFinset_empty {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_2} [inst : Nonempty α] :
@[simp]
theorem Fintype.piFinset_singleton {α : Type u_1} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_2} (f : (i : α) → δ i) :
(Fintype.piFinset fun i => {f i}) = {f}
theorem Fintype.piFinset_subsingleton {α : Type u_2} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_1} {f : (i : α) → Finset (δ i)} (hf : ∀ (i : α), Set.Subsingleton ↑(f i)) :
theorem Fintype.piFinset_disjoint_of_disjoint {α : Type u_2} [inst : DecidableEq α] [inst : Fintype α] {δ : αType u_1} (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) {a : α} (h : Disjoint (t₁ a) (t₂ a)) :

pi #

instance Pi.fintype {α : Type u_1} {β : αType u_2} [inst : DecidableEq α] [inst : Fintype α] [inst : (a : α) → Fintype (β a)] :
Fintype ((a : α) → β a)

A dependent product of fintypes, indexed by a fintype, is a fintype.

Equations
@[simp]
theorem Fintype.piFinset_univ {α : Type u_1} {β : αType u_2} [inst : DecidableEq α] [inst : Fintype α] [inst : (a : α) → Fintype (β a)] :
(Fintype.piFinset fun a => Finset.univ) = Finset.univ
noncomputable instance Function.Embedding.fintype {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst : Fintype β] :
Fintype (α β)
Equations
@[simp]
theorem Finset.univ_pi_univ {α : Type u_1} {β : αType u_2} [inst : DecidableEq α] [inst : Fintype α] [inst : (a : α) → Fintype (β a)] :
(Finset.pi Finset.univ fun a => Finset.univ) = Finset.univ