closure_le_iff — Mathlib

English

If y is closed, then for all x, c x ≤ y iff x ≤ y.

Русский

Если y замкнуто, то для всех x выполнено c x ≤ y эквивалентно x ≤ y.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] {c : ClosureOperator {\\\\alpha}} {x y : {\\\\alpha}},\\\\; (hy : c.IsClosed y) \\\\Rightarrow (c x \\\\le y \\\\Longleftrightarrow x \\\\le y)$$$

Lean4

@[simp]
theorem closure_le_iff (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y := by rw [← hy.closure_eq, ← le_closure_iff]

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