isClosed_iff_closure_le — Mathlib

English

An element x is closed iff its closure is below or equal to x: c.IsClosed x ⇔ c x ≤ x.

Русский

Элемент x замкнут относительно c тогда и только тогда, когда c x ≤ x.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] {c : ClosureOperator {\\\\alpha}} {x : {\\\\alpha}}, c.IsClosed x \\\\leftrightarrow c x \\\\le x$$$

Lean4

theorem isClosed_iff_closure_le : c.IsClosed x ↔ c x ≤ x :=
  ⟨fun h ↦ h.closure_eq.le, fun h ↦ c.isClosed_iff.2 <| h.antisymm <| c.le_closure x⟩

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