Fintype instances for pi types #
def
Fintype.piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
(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.univ.pi t)
@[simp]
theorem
Fintype.mem_piFinset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
{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_4}
(t : (a : α) → Finset (δ a))
:
↑(Fintype.piFinset t) = Set.univ.pi fun (a : α) => ↑(t a)
theorem
Fintype.piFinset_subset
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
(t₁ : (a : α) → Finset (δ a))
(t₂ : (a : α) → Finset (δ a))
(h : ∀ (a : α), t₁ a ⊆ t₂ a)
:
@[simp]
theorem
Fintype.piFinset_eq_empty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_3}
{s : (a : α) → Finset (γ a)}
:
@[simp]
theorem
Fintype.piFinset_empty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
[Nonempty α]
:
(Fintype.piFinset fun (x : α) => ∅) = ∅
@[simp]
theorem
Fintype.piFinset_nonempty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_3}
{s : (a : α) → Finset (γ a)}
:
(Fintype.piFinset s).Nonempty ↔ ∀ (a : α), (s a).Nonempty
theorem
Fintype.Aesop.piFinset_nonempty_of_forall_nonempty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_3}
{s : (a : α) → Finset (γ a)}
:
(∀ (a : α), (s a).Nonempty) → (Fintype.piFinset s).Nonempty
Alias of the reverse direction of Fintype.piFinset_nonempty.
theorem
Finset.Nonempty.piFinset_const
{β : Type u_2}
{ι : Type u_5}
[Fintype ι]
[DecidableEq ι]
{s : Finset β}
(hs : s.Nonempty)
:
(Fintype.piFinset fun (x : ι) => s).Nonempty
@[simp]
theorem
Fintype.piFinset_of_isEmpty
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{γ : α → Type u_3}
[IsEmpty α]
(s : (a : α) → Finset (γ a))
:
Fintype.piFinset s = Finset.univ
@[simp]
theorem
Fintype.piFinset_singleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
(f : (i : α) → δ i)
:
(Fintype.piFinset fun (i : α) => {f i}) = {f}
theorem
Fintype.piFinset_subsingleton
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
{f : (i : α) → Finset (δ i)}
(hf : ∀ (i : α), (↑(f i)).Subsingleton)
:
(↑(Fintype.piFinset f)).Subsingleton
theorem
Fintype.piFinset_disjoint_of_disjoint
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
(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_3}
{δ : α → Type u_4}
[(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_4}
(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_4}
(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_5}
[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_4}
[(a : α) → DecidableEq (δ a)]
(t : (a : α) → Finset (δ a))
(a : α)
(x : δ a)
(hx : x ∉ t a)
:
Finset.filter (fun (f : (a : α) → δ a) => f a = x) (Fintype.piFinset t) = ∅
theorem
Fintype.piFinset_update_eq_filter_piFinset_mem
{α : Type u_1}
[DecidableEq α]
[Fintype α]
{δ : α → Type u_4}
[(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_4}
[(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_3}
{β : α → Type u_4}
[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_3}
{β : α → Type u_4}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
:
(Fintype.piFinset fun (a : α) => Finset.univ) = Finset.univ
noncomputable instance
Function.Embedding.fintype
{α : Type u_3}
{β : Type u_4}
[Fintype α]
[Fintype β]
:
Equations
- Function.Embedding.fintype = Fintype.ofEquiv { f : α → β // Function.Injective f } (Equiv.subtypeInjectiveEquivEmbedding α β)
instance
RelHom.instFintype
{α : Type u_3}
{β : Type u_4}
[Fintype α]
[Fintype β]
[DecidableEq α]
{r : α → α → Prop}
{s : β → β → Prop}
[DecidableRel r]
[DecidableRel s]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Finset.univ_pi_univ
{α : Type u_3}
{β : α → Type u_4}
[DecidableEq α]
[Fintype α]
[(a : α) → Fintype (β a)]
:
(Finset.univ.pi fun (a : α) => Finset.univ) = Finset.univ
Diagonal #
theorem
Finset.piFinset_filter_const
{α : Type u_1}
{ι : Type u_3}
[DecidableEq (ι → α)]
{s : Finset α}
[DecidableEq ι]
[Fintype ι]
:
Finset.filter (fun (f : ι → α) => ∃ a ∈ s, Function.const ι a = f) (Fintype.piFinset fun (x : ι) => s) = s.piDiag ι
theorem
Finset.piDiag_subset_piFinset
{α : Type u_1}
{ι : Type u_3}
[DecidableEq (ι → α)]
{s : Finset α}
[DecidableEq ι]
[Fintype ι]
:
s.piDiag ι ⊆ Fintype.piFinset fun (x : ι) => s