bounded_le_inter_le — Mathlib

English

For α linear order, a, the intersection s ∩ { b | a ≤ b } is bounded below with respect to ≤ if and only if s is bounded below.

Русский

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

LaTeX

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

Lean4

theorem bounded_le_inter_le [LinearOrder α] (a : α) : Bounded (· ≤ ·) (s ∩ {b | a ≤ b}) ↔ Bounded (· ≤ ·) s :=
  by
  refine ⟨?_, Bounded.mono Set.inter_subset_left⟩
  rw [← @bounded_le_inter_lt _ s _ a]
  exact Bounded.mono fun x ⟨hx, hx'⟩ => ⟨hx, le_of_lt hx'⟩

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