toFinset_Icc — Mathlib

English

In a lattice with LocallyFiniteOrder, a set s is finite iff it is both bounded below and bounded above.

Русский

В решётке с локально конечным порядком множество конечное тогда и только тогда, когда оно ограничено снизу и сверху.

LaTeX

$$$s\\text{ finite} \\iff (BddBelow(s) \\land BddAbove(s))$$$

Lean4

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

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