not_lt_of_denselyOrdered_of_locallyFinite

English

In a densely ordered, locally finite order, there are no strict inequalities between any two elements; i.e., for all a,b, ¬(a < b).

Русский

В плотно упорядоченном локально конечном порядке для любых a,b неверно a < b.

LaTeX

$$$ \forall a,b \in \alpha, \; \neg (a < b) \; (\text{при} \; [DenselyOrdered(\alpha)]).$$$

Lean4

theorem _root_.not_lt_of_denselyOrdered_of_locallyFinite [DenselyOrdered α] (a b : α) : ¬a < b :=
  by
  intro h
  induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with
  | H i ih
  subst hs
  obtain ⟨c, hac, hcb⟩ := exists_between h
  refine ih _ ?_ c hac rfl
  exact Finset.Icc_ssubset_Icc_right (hac.trans hcb).le le_rfl hcb

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