fintype instances for pi types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
fintype.pi_finset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(t : Π (a : α), finset (δ a)) :
Given for all a : α a finset t a of δ a, then one can define the
finset fintype.pi_finset 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.pi_finset t = finset.map {to_fun := λ (f : Π (a : α), a ∈ finset.univ → δ a) (a : α), f a _, inj' := _} (finset.univ.pi t)
@[simp]
theorem
fintype.mem_pi_finset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
{t : Π (a : α), finset (δ a)}
{f : Π (a : α), δ a} :
f ∈ fintype.pi_finset t ↔ ∀ (a : α), f a ∈ t a
@[simp]
theorem
fintype.coe_pi_finset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(t : Π (a : α), finset (δ a)) :
theorem
fintype.pi_finset_subset
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(t₁ t₂ : Π (a : α), finset (δ a))
(h : ∀ (a : α), t₁ a ⊆ t₂ a) :
@[simp]
theorem
fintype.pi_finset_empty
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
[nonempty α] :
fintype.pi_finset (λ (_x : α), ∅) = ∅
@[simp]
theorem
fintype.pi_finset_singleton
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(f : Π (i : α), δ i) :
fintype.pi_finset (λ (i : α), {f i}) = {f}
theorem
fintype.pi_finset_subsingleton
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
{f : Π (i : α), finset (δ i)}
(hf : ∀ (i : α), ↑(f i).subsingleton) :
theorem
fintype.pi_finset_disjoint_of_disjoint
{α : Type u_1}
[decidable_eq α]
[fintype α]
{δ : α → Type u_2}
(t₁ t₂ : Π (a : α), finset (δ a))
{a : α}
(h : disjoint (t₁ a) (t₂ a)) :
disjoint (fintype.pi_finset t₁) (fintype.pi_finset t₂)
pi #
@[protected, instance]
def
pi.fintype
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
[fintype α]
[Π (a : α), fintype (β a)] :
A dependent product of fintypes, indexed by a fintype, is a fintype.
Equations
- pi.fintype = {elems := fintype.pi_finset (λ (_x : α), finset.univ), complete := _}
@[simp]
theorem
fintype.pi_finset_univ
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
[fintype α]
[Π (a : α), fintype (β a)] :
fintype.pi_finset (λ (a : α), finset.univ) = finset.univ
@[protected, instance]
def
function.embedding.fintype
{α : Type u_1}
{β : Type u_2}
[fintype α]
[fintype β]
[decidable_eq α]
[decidable_eq β] :
Equations
@[simp]
theorem
finset.univ_pi_univ
{α : Type u_1}
{β : α → Type u_2}
[decidable_eq α]
[fintype α]
[Π (a : α), fintype (β a)] :
finset.univ.pi (λ (a : α), finset.univ) = finset.univ