bounded_le_iff_bounded_lt — Mathlib

English

If s is bounded for <, then it is bounded for ≤, and conversely in NoMaxOrder.

Русский

Если s ограничено по <, то ограничено и по ≤; в NoMaxOrder симметрично.

LaTeX

$$Bounded(<, s) ⇒ Bound(≤, s) and Bound(≤, s) ⇒ Bound(<, s) (NoMaxOrder)$$

Lean4

theorem bounded_le_iff_bounded_lt [Preorder α] [NoMaxOrder α] : Bounded (· ≤ ·) s ↔ Bounded (· < ·) s :=
  by
  refine ⟨fun h => ?_, bounded_le_of_bounded_lt⟩
  obtain ⟨a, ha⟩ := h
  obtain ⟨b, hb⟩ := exists_gt a
  exact ⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩

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