unbounded_le_inter_lt — Mathlib

English

Let α be a linear order. For a, the unboundedness of s ∩ { b | a ≤ b } with respect to ≤ is equivalent to the unboundedness of s.

Русский

Пусть α линейный порядок. Неограниченность s ∩ { b | a ≤ b } по ≤ эквивалентна неограниченности s.

LaTeX

$$$$\mathrm{Unbounded}_{\le}\left(s \cap \{b \mid a \le b\}\right) \iff \mathrm{Unbounded}_{\le}(s).$$$$

Lean4

theorem unbounded_le_inter_lt [LinearOrder α] (a : α) : Unbounded (· ≤ ·) (s ∩ {b | a < b}) ↔ Unbounded (· ≤ ·) s :=
  by
  convert @unbounded_le_inter_not_le _ s _ a
  exact lt_iff_not_ge

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