piFinset_subsingleton — Mathlib

English

If each coordinate set f(i) is a Subsingleton, then the piFinset is a Subsingleton.

Русский

Если на каждой координате множество — подмножество одного элемента, то piFinset также является подмножеством одного элемента.

LaTeX

$$$\\bigl( \\forall a, (f(a) : Set(\\delta a)).Subsingleton \\bigr) \\Rightarrow (\\operatorname{piFinset} f).toSet.Subsingleton.$$$

Lean4

theorem piFinset_subsingleton {f : ∀ i, Finset (δ i)} (hf : ∀ i, (f i : Set (δ i)).Subsingleton) :
    (Fintype.piFinset f : Set (∀ i, δ i)).Subsingleton := fun _ ha _ hb =>
  funext fun _ => hf _ (mem_piFinset.1 ha _) (mem_piFinset.1 hb _)

Похожие утверждения