le_closure_iff — Mathlib

English

For all x, y, x ≤ c(y) if and only if c(x) ≤ c(y).

Русский

Для любых x, y выполняется x ≤ c(y) тогда и только тогда, когда c(x) ≤ c(y).

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] \\\\forall {c : ClosureOperator {\\\\alpha}} \\\\forall {x y : {\\\\alpha}}, x \\\\le c y \\\\Longleftrightarrow c x \\\\le c y$$$

Lean4

theorem le_closure_iff : x ≤ c y ↔ c x ≤ c y :=
  ⟨fun h ↦ c.idempotent y ▸ c.monotone h, (c.le_closure x).trans⟩

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