closure_sup_closure — Mathlib

English

For c on a semilattice with sup, c(x) ∨ c(y) equals c(x ∨ y) up to equality of images.

Русский

Для замыкателя на полупорядоченном множестве с суммой выполняется равенство между образами и образ суммы.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [SemilatticeSup {\\\\alpha}] (c : ClosureOperator {\\\\alpha}) \\\\forall x y : {\\\\alpha}, c x \\\\lor c y = c (x \\\\lor y)$$$

Lean4

theorem closure_sup_closure (x y : α) : c (c x ⊔ c y) = c (x ⊔ y) := by
  rw [closure_sup_closure_left, closure_sup_closure_right]

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