toFinset_Ico — Mathlib

English

For a,b ∈ α with LocallyFiniteOrder, the Finset representation of the closed interval Icc(a,b) agrees with the standard Finset Icc.

Русский

Для a,b ∈ α при локально конечном порядке отображение множества Icc(a,b) в Finset совпадает с обычным Finset Icc.

LaTeX

$$$(\\mathrm{Icc}(a,b)).\\mathrm{toFinset} = \\mathrm{Finset.Icc}(a,b)$$$

Lean4

@[simp]
theorem toFinset_Ico (a b : α) [Fintype (Ico a b)] : (Ico a b).toFinset = Finset.Ico a b := by ext; simp

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