subset_toFinset — Mathlib

English

Let s be a finite subset (as a Finset) of α and t a finite subset of α. Then s is contained in the Finset ht.toFinset iff the underlying set ↑s is contained in t.

Русский

Пусть s — конечное подмножество α (в виде Finset), а t — конечное подмножество α. Тогда s ⊆ ht.toFinset тогда и только если множество ↑s ⊆ t.

LaTeX

$$$ s \subseteq ht.toFinset \Longleftrightarrow \uparrow s \subseteq t $$$

Lean4

@[simp]
theorem subset_toFinset {s : Finset α} : s ⊆ ht.toFinset ↔ ↑s ⊆ t := by rw [← Finset.coe_subset, Finite.coe_toFinset]

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