insert_upperBounds — Mathlib

English

If s is sup-closed and a is an upper 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_upperBounds {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) : SupClosed (insert a s) :=
  by
  rw [SupClosed]
  aesop

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