coe_ssubset — Mathlib

English

The strict subset relation for Finset α corresponds to the strict inclusion of their underlying sets.

Русский

Строгое включение Finset α соответствует строгому включению их отображённых множеств.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_ssubset {s₁ s₂ : Finset α} : (s₁ : Set α) ⊂ s₂ ↔ s₁ ⊂ s₂ :=
  show (s₁ : Set α) ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁ by simp only [Set.ssubset_def, Finset.coe_subset]

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