unbounded_inter_ge — Mathlib

English

In a linear order α, Unbounded (GT) on s ∩ {b | b ≤ a} is equivalent to Unbounded GT on s.

Русский

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

LaTeX

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

Lean4

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

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