sup_mem_supClosure — Mathlib

English

If a and b belong to s, then their join a ⊔ b belongs to supClosure(s).

Русский

Если a и b принадлежат s, то их наибольший низший элемент a ⊔ b принадлежит supClosure(s).

LaTeX

$$$a,b \\in s \\Rightarrow a \\sqcup b \\in \\operatorname{supClosure}(s)$$$

Lean4

theorem sup_mem_supClosure (ha : a ∈ s) (hb : b ∈ s) : a ⊔ b ∈ supClosure s :=
  supClosed_supClosure (subset_supClosure ha) (subset_supClosure hb)

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