toFinset_Ioo — Mathlib

English

For a,b ∈ α with LocallyFiniteOrder, the Finset representation of Ioo(a,b) equals Finset.Ioo(a,b).

Русский

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

LaTeX

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

Lean4

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

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