coe_subset_singleton — Mathlib

English

The inclusion relation is preserved by the coercion: (s : Set α) ⊆ {a} if and only if s ⊆ {a} as finsets.

Русский

Отношение включения сохраняется под приведением: (s : Set α) ⊆ {a} тогда и только тогда, когда s ⊆ {a} как Finset.

LaTeX

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

Lean4

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

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