bounded_lt_Iic — Mathlib

English

For any a, the set { x ∈ α | x ≤ a } is bounded with respect to <, provided NoMaxOrder.

Русский

Для каждого a множество { x ∈ α | x ≤ a } ограничено сверху по отношению < при условии NoMaxOrder.

LaTeX

$$$\forall a:\ Bound\ ed\ (<)\ (Iic\ a)$$$

Lean4

theorem bounded_lt_Iic [Preorder α] [NoMaxOrder α] (a : α) : Bounded (· < ·) (Iic a) := by
  simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]

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