closure_sup_closure_left — Mathlib

English

For x,y in a semilattice with sup, c(x ∨ c y) = c(x ∨ y).

Русский

Для любых x,y в полупорядоченном множестве с верхом: c(x ∨ c y) = c(x ∨ y).

LaTeX

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

Lean4

theorem closure_sup_closure_left (x y : α) : c (c x ⊔ y) = c (x ⊔ y) :=
  le_antisymm (le_closure_iff.1 (sup_le (c.monotone le_sup_left) (le_sup_right.trans (c.le_closure _))))
    (by grw [← c.le_closure x])

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