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.

@[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) : Fintype.piFinset t₁ ⊆ Fintype.piFinset t₂

@[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)) : Set.Subsingleton ↑(Fintype.piFinset f)

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 β] : 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)] : (Finset.pi Finset.univ fun (a : α) => Finset.univ) = Finset.univ

theorem Fin.mem_piFinset_succ_iff {n : ℕ} {α : Fin (n + 1) → Type u_2} (p : (i : Fin (n + 1)) → α i) (S : (i : Fin (n + 1)) → Finset (α i)) : p ∈ Fintype.piFinset S ↔ p 0 ∈ S 0 ∧ Fin.tail p ∈ Fintype.piFinset (Fin.tail S)

theorem Fin.cons_mem_piFinset_cons_iff {n : ℕ} {α : Fin (n + 1) → Type u_2} (x : α 0) (xs : (i : Fin n) → α (Fin.succ i)) (S₀ : Finset (α 0)) (Sᵢ : (i : Fin n) → Finset (α (Fin.succ i))) : Fin.cons x xs ∈ Fintype.piFinset (Fin.cons S₀ Sᵢ) ↔ x ∈ S₀ ∧ xs ∈ Fintype.piFinset Sᵢ

theorem Fin.mem_piFinset_succ_iff' {n : ℕ} {α : Fin (n + 1) → Type u_2} (p : (i : Fin (n + 1)) → α i) (S : (i : Fin (n + 1)) → Finset (α i)) : p ∈ Fintype.piFinset S ↔ Fin.init p ∈ Fintype.piFinset (Fin.init S) ∧ p (Fin.last n) ∈ S (Fin.last n)

theorem Fin.snoc_mem_piFinset_snoc_iff {n : ℕ} {α : Fin (n + 1) → Type u_2} (xs : (i : Fin n) → α (Fin.castSucc i)) (x : α (Fin.last n)) (Sᵢ : (i : Fin n) → Finset (α (Fin.castSucc i))) (Sₙ : Finset (α (Fin.last n))) : Fin.snoc xs x ∈ Fintype.piFinset (Fin.snoc Sᵢ Sₙ) ↔ xs ∈ Fintype.piFinset Sᵢ ∧ x ∈ Sₙ