csInf_Ioi — Mathlib

English

In any densely ordered lattice with no maximum, the infimum of the open interval Ioi(a) is a.

Русский

В плоскости без максима и плотной упорядоченности инфимуум открытого интервала Ioi(a) равен a.

LaTeX

$$$\forall \alpha\ [\text{NoMaxOrder }\alpha] [\text{DenselyOrdered }\alpha],\ sInf(Ioi(a)) = a$$$

Lean4

@[simp]
theorem csInf_Ioi [NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a :=
  csInf_eq_of_forall_ge_of_forall_gt_exists_lt nonempty_Ioi (fun _ => le_of_lt) fun w hw => by
    simpa using exists_between hw

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