ofFiniteIcc — Mathlib

English

If every closed interval Icc(a,b) is finite, then α can be equipped with a LocallyFiniteOrder structure.

Русский

Если каждый закрытый интервал Icc(a,b) конечен, то α можно снабдить структурой локально конечного порядка.

LaTeX

$$$\big( \forall a,b \in \alpha, \lvert Icc(a,b) \rvert < \infty \big) \Rightarrow \mathrm{LocallyFiniteOrder}(\alpha)$$$

Lean4

/-- A noncomputable constructor from the finiteness of all closed intervals. -/
noncomputable def ofFiniteIcc (h : ∀ a b : α, (Set.Icc a b).Finite) : LocallyFiniteOrder α :=
  @LocallyFiniteOrder.ofIcc' α _ (Classical.decRel _) (fun a b => (h a b).toFinset) fun a b x => by
    rw [Set.Finite.mem_toFinset, Set.mem_Icc]

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