insert_lowerBounds — Mathlib

English

If s is sup-closed and a is a lower bound of s, then inserting a into s yields a sup-closed set.

Русский

Если s замкнуто по ⊔ и a является нижней границей множества s, то добавление a в s сохраняет sup-замкнутость.

LaTeX

$$$ (\\forall x \\in s)(\\forall y \\in s)\\, x \\sqcup y \\in s \\Rightarrow (\\forall x \\in \\operatorname{insert}(a,s))(\\forall y \\in \\operatorname{insert}(a,s))\\, x \\sqcup y \\in \\operatorname{insert}(a,s) $$$

Lean4

theorem insert_lowerBounds {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) : SupClosed (insert a s) :=
  by
  rw [SupClosed]
  have ha' : ∀ b ∈ s, a ≤ b := fun _ a ↦ ha a
  aesop

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