toFinset_subset_toFinset — Mathlib

English

For finite s and t, the Finset inclusion hs.toFinset ⊆ ht.toFinset is equivalent to the set inclusion s ⊆ t.

Русский

Для конечных множеств s и t проверка, что toFinset s содержится в toFinset t, эквивалентна включению множеств s ⊆ t.

LaTeX

$$$ (hs.toFinset \subseteq ht.toFinset) \Longleftrightarrow (s \subseteq t) $$$

Lean4

@[mono]
protected theorem toFinset_subset_toFinset : hs.toFinset ⊆ ht.toFinset ↔ s ⊆ t := by
  simp only [← Finset.coe_subset, Finite.coe_toFinset]

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