singleton_subset_coe — Mathlib

English

The singleton {a} is contained in s as a set if and only if {a} is contained in s as a finset.

Русский

Единственный элемент {a} принадлежит s как множеству тогда и только тогда, когда {a} принадлежит s как Finset.

LaTeX

$$$\{ a \} \subseteq (s : \mathrm{Set} \alpha) \iff \{ a \} \subseteq s$$$

Lean4

@[norm_cast]
theorem singleton_subset_coe : { a } ⊆ (s : Set α) ↔ { a } ⊆ s := by grind

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