bounded_le_inter_lt — Mathlib

English

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

Русский

При линейном порядке α, множество 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_le_inter_lt [LinearOrder α] (a : α) : Bounded (· ≤ ·) (s ∩ {b | a < b}) ↔ Bounded (· ≤ ·) s := by
  simp_rw [← not_le, bounded_le_inter_not_le]

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