unbounded_ge_inter_gt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem unbounded_ge_inter_gt [LinearOrder α] (a : α) : Unbounded (· ≥ ·) (s ∩ {b | b < a}) ↔ Unbounded (· ≥ ·) s :=
  @unbounded_le_inter_lt αᵒᵈ s _ a

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