closure_inf_le — Mathlib

English

For a closure operator c on a semilattice with inf, c(x ∧ y) ≤ c(x) ∧ c(y).

Русский

Для замыкателя c на частично упорядоченном линейном пространстве с операцией meet выполняется c(x ∧ y) ≤ c(x) ∧ c(y).

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [SemilatticeInf {\\\\alpha}] (c : ClosureOperator {\\\\alpha}) \\\\forall x y : {\\\\alpha}, c (x \\\\_and y) \\\\le c x \\\\wedge c y$$$

Lean4

theorem closure_inf_le [SemilatticeInf α] (c : ClosureOperator α) (x y : α) : c (x ⊓ y) ≤ c x ⊓ c y :=
  c.monotone.map_inf_le _ _

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