fintypeUIcc — Mathlib

English

In a lattice with a locally finite order, the interval between any two elements is finite.

Русский

В решетке с локально конечным порядком промежуток между любыми двумя элементами конечен.

LaTeX

$$$\forall a,b, \lvert \{ x \in \alpha \mid \min(a,b) \le x \le \max(a,b) \} \rvert < \infty$$$

Lean4

instance fintypeUIcc : Fintype (uIcc a b) :=
  Fintype.ofFinset (Finset.uIcc a b) fun _ => Finset.mem_uIcc

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