ssubset_toFinset — Mathlib

English

Let s be a Finset α and ht a finite subset t of α. Then s is a strict subset of ht.toFinset iff ↑s is a strict subset of t.

Русский

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

LaTeX

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

Lean4

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

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