unbounded_lt_inter_le — Mathlib

English

In a linear order with no maximum, the set s ∩ { b | a < b } is unbounded with respect to < if and only if s is unbounded with respect to <.

Русский

В линейном порядке без максимального элемента множество s ∩ { b | a < b } не ограничено снизу относительно < тогда и только тогда, когда s не ограничено снизу относительно <.

LaTeX

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

Lean4

theorem unbounded_lt_inter_le [LinearOrder α] (a : α) : Unbounded (· < ·) (s ∩ {b | a ≤ b}) ↔ Unbounded (· < ·) s :=
  by
  convert @unbounded_lt_inter_not_lt _ s _ a
  exact not_lt.symm

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