denselyOrdered_iff_forall_not_covBy

English

A densely ordered set is equivalent to: for all a,b, not a CovBy b.

Русский

Плотный порядок эквивалентен: для всех a,b не выполняется a CovBy b.

LaTeX

$$$$\text{DenselyOrdered }\alpha \iff \forall a,b:\alpha,\neg(a\lessdot b).$$$$

Lean4

theorem denselyOrdered_iff_forall_not_covBy : DenselyOrdered α ↔ ∀ a b : α, ¬a ⋖ b :=
  ⟨fun h _ _ => @not_covBy _ _ _ _ h, fun h => ⟨fun _ _ hab => exists_lt_lt_of_not_covBy hab <| h _ _⟩⟩

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