English
Let α be a semilattice with inf. If s ⊆ α is InfClosed and a is an upper bound of s, then the set obtained by inserting a into s is InfClosed.
Русский
Пусть α — полузаданное множество с операцией inf. Если s ⊆ α удовлетворяет InfClosed и a является верхней границей множества s, то множество, полученное путем добавления a к s, сохраняет свойство InfClosed.
LaTeX
$$$\\forall \\alpha\\ [\\text{SemilatticeInf } \\alpha],\\ s:\\ Set\\ \\alpha,\\ a:\\alpha,\\ InfClosed\\ s \\land a \\in upperBounds\\ s \\Rightarrow InfClosed\\ (insert\\ a\\ s)$$$
Lean4
theorem insert_upperBounds {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) : InfClosed (insert a s) :=
by
rw [InfClosed]
have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
aesop
