insert_lowerBounds — Mathlib

English

Let α be a semilattice with inf. If s ⊆ α is InfClosed and a is a lower bound of s, then the set obtained by inserting a into s is InfClosed.

Русский

Пусть α — полузаданное множество с Inf. Если s является InfClosed и a является нижней границей множества s, то s ∪ {a} сохраняет InfClosed.

LaTeX

$$$\\forall \\alpha\\ [\\text{SemilatticeInf } \\alpha],\\ s:\\ Set\\ \\alpha,\\ a:\\alpha,\\ InfClosed\\ s \\land a \\in lowerBounds\\ s \\Rightarrow InfClosed\\ (insert\\ a\\ s)$$$

Lean4

theorem insert_lowerBounds {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) : InfClosed (insert a s) :=
  by
  rw [InfClosed]
  aesop

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