toFinset_Ioc — Mathlib

English

For a,b ∈ α with LocallyFiniteOrder, the Finset representation of the half-open interval Ico(a,b) matches Finset.Ico(a,b).

Русский

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

LaTeX

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

Lean4

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

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