bounded_ge_inter_gt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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