bounded_le_inter_not_le — Mathlib

English

Let α be a semilattice with join, and a ∈ α. Then Bounded (≤) on s ∩ {b : ¬ b ≤ a} is equivalent to Bounded (≤) on s.

Русский

Пусть α имеет полусложение, и a ∈ α. Тогда Bound_≤(s ∩ { b | ¬ b ≤ a }) эквивалентен Bound_≤(s).

LaTeX

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

Lean4

theorem bounded_le_inter_not_le [SemilatticeSup α] (a : α) : Bounded (· ≤ ·) (s ∩ {b | ¬b ≤ a}) ↔ Bounded (· ≤ ·) s :=
  bounded_inter_not (fun x y => ⟨x ⊔ y, fun _ h => h.elim le_sup_of_le_left le_sup_of_le_right⟩) a

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