bounded_lt_inter_le — Mathlib

English

In a linear order α, for a given a, the intersection s ∩ { b | a ≤ b } is bounded with respect to the strict order < if and only if s is bounded with respect to <.

Русский

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

LaTeX

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

Lean4

theorem bounded_lt_inter_le [LinearOrder α] (a : α) : Bounded (· < ·) (s ∩ {b | a ≤ b}) ↔ Bounded (· < ·) s :=
  by
  convert @bounded_lt_inter_not_lt _ s _ a
  exact not_lt.symm

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