coe_subset — Mathlib

English

Viewing a finite set as a subset of α preserves the subset relation with another finite set.

Русский

Рассматривая конечное множество как подмножество α, сохраняется отношение ⊆ по отношению к другому конечному множеству.

LaTeX

$$$(s_1 : Set\ α) \subseteq s_2 \iff s_1 \subseteq s_2$$$

Lean4

@[simp, norm_cast]
theorem coe_subset {s₁ s₂ : Finset α} : (s₁ : Set α) ⊆ s₂ ↔ s₁ ⊆ s₂ :=
  Iff.rfl

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