noBotOrder_iff_noMinOrder — Mathlib

English

For linear orders, NoBotOrder α is equivalent to NoMinOrder α.

Русский

Для линейного порядка отсутствие нижнего элемента эквивалентно отсутствию минимума.

LaTeX

$$$\text{NoBotOrder}(\alpha) \iff \text{NoMinOrder}(\alpha)$$$

Lean4

theorem noBotOrder_iff_noMinOrder (α : Type*) [LinearOrder α] : NoBotOrder α ↔ NoMinOrder α :=
  ⟨fun _ => NoBotOrder.to_noMinOrder α, fun _ => inferInstance⟩

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