English
The subsingleton property of a set’s elements is equivalent to the set being subsingleton as a subset.
Русский
Свойство подсинглотонности множества его элементов эквивалентно тому, что множество как подмножество — подсинглотон.
LaTeX
$$$ \text{subsingleton_coe } (s) : Subsingleton s.Elem \iff s.Subsingleton $$$
Lean4
/-- `s`, coerced to a type, is a subsingleton type if and only if `s` is a subsingleton set. -/
@[simp, norm_cast]
theorem subsingleton_coe (s : Set α) : Subsingleton s ↔ s.Subsingleton :=
by
constructor
· refine fun h => fun a ha b hb => ?_
exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
· exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)
