unbounded_gt_inter_gt — Mathlib

English

In a linear order α with NoMinOrder property, Unbounded (>) on s ∩ {b | b < a} is equivalent to Unbounded (>) on s.

Русский

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

LaTeX

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

Lean4

theorem unbounded_gt_inter_gt [LinearOrder α] [NoMinOrder α] (a : α) :
    Unbounded (· > ·) (s ∩ {b | b < a}) ↔ Unbounded (· > ·) s :=
  @unbounded_lt_inter_lt αᵒᵈ s _ _ a

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