bounded_lt_inter_not_lt — Mathlib

English

For a linear order α, a, the intersection s ∩ { b | a < b } bounded below is equivalent to s being bounded below.

Русский

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

LaTeX

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

Lean4

theorem bounded_lt_inter_not_lt [SemilatticeSup α] (a : α) : Bounded (· < ·) (s ∩ {b | ¬b < a}) ↔ Bounded (· < ·) s :=
  bounded_inter_not (fun x y => ⟨x ⊔ y, fun _ h => h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩) a

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