closure_sup_closure_le — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem closure_sup_closure_le (x y : α) : c x ⊔ c y ≤ c (x ⊔ y) :=
  c.monotone.le_map_sup _ _

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