unbounded_le_inter_not_le — Mathlib

English

Let α be a semilattice with join. For a fixed a, Unbounded (≤) on s ∩ {b : ¬ b ≤ a} holds if and only if Unbounded (≤) on s holds.

Русский

Пусть α имеет символьное объединение; для фиксированного a, Unbounded_≤(s ∩ {b | ¬ b ≤ a}) эквивалентно Unbounded_≤(s).

LaTeX

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

Lean4

theorem unbounded_le_inter_not_le [SemilatticeSup α] (a : α) :
    Unbounded (· ≤ ·) (s ∩ {b | ¬b ≤ a}) ↔ Unbounded (· ≤ ·) s :=
  by
  rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
  exact bounded_le_inter_not_le a

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