unbounded_ge_iff_unbounded_inter_ge

English

In a linear order, having no lower bound for s ∩ {b ≤ a} is equivalent to having no lower bound for s.

Русский

В линейном порядке отсутствие нижней границы для s ∩ {b ≤ a} эквивалентно отсутствию нижней границы для s.

LaTeX

$$$\forall m\, \exists x\in s\cap\{y\;|\; y\le a\},\; x

Lean4

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

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