unbounded_le_inter_le — Mathlib

English

Let α be a linear order. For a, Unbounded (≤) on s ∩ { b | a ≤ b } is equivalent to Unbounded (≤) on 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_le [LinearOrder α] (a : α) : Unbounded (· ≤ ·) (s ∩ {b | a ≤ b}) ↔ Unbounded (· ≤ ·) s :=
  by
  rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_le_inter_le a

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