English
In a linear order α with NoMaxOrder, for any a, the set s ∩ { b | a < b } is bounded with respect to < if and only if s is bounded with respect to <.
Русский
Для линейного порядка α с NoMaxOrder при любом a множество s ∩ { b | a < b } ограничено снизу относительно < тогда и только тогда, когда s ограничено снизу относительно <.
LaTeX
$$$$\mathrm{Bounded}_{<}\left(s \cap \{b \mid a < b\}\right) \iff \mathrm{Bounded}_{<}(s).$$$$
Lean4
theorem bounded_lt_inter_lt [LinearOrder α] [NoMaxOrder α] (a : α) :
Bounded (· < ·) (s ∩ {b | a < b}) ↔ Bounded (· < ·) s :=
by
rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]
exact bounded_le_inter_lt a
