English
Let the ambient set lie in a linearly ordered type. For any subset s and any a, the set s ∩ {b ≤ a} is bounded below with respect to ≥ if and only if s is bounded below with respect to ≥.
Русский
Пусть окружение задаётся линейно упорядоченным множеством. Тогда для любого множества s и любого a множество s ∩ {b ≤ a} ограничено снизу по отношению ≥ тогда и только тогда, когда ограничено снизу по отношению ≥ множество s.
LaTeX
$$$\exists m\, \forall x\in s\cap\{y\;|\; y\le a\},\; m\le x \;\Longleftrightarrow\; \exists m\, \forall x\in s,\; m\le x$$$
Lean4
theorem bounded_ge_inter_ge [LinearOrder α] (a : α) : Bounded (· ≥ ·) (s ∩ {b | b ≤ a}) ↔ Bounded (· ≥ ·) s :=
@bounded_le_inter_le αᵒᵈ s _ a
