bounded_gt_inter_gt — Mathlib

English

Let α be a linear order with a no-minimum property. The set s ∩ {b | b < a} is bounded above with respect to > iff s is bounded above with respect to >.

Русский

Пусть α — линейный порядок с отсутствием минимального элемента. Множество s ∩ {b | b < a} ограничено сверху по отношению > тогда и только тогда, когда s ограничено сверху по отношению >.

LaTeX

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

Lean4

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

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