unbounded_lt_inter_lt — Mathlib

English

Let α be a linear order with NoMaxOrder. Then Unbounded (lt) on s ∩ { b | a < b } is equivalent to Unbounded lt on s.

Русский

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

LaTeX

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

Lean4

theorem unbounded_lt_inter_lt [LinearOrder α] [NoMaxOrder α] (a : α) :
    Unbounded (· < ·) (s ∩ {b | a < b}) ↔ Unbounded (· < ·) s :=
  by
  rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_lt_inter_lt a

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