closure_isGLB — Mathlib

English

For every x, c(x) is the greatest lower bound of all closed y with x ≤ y.

Русский

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

LaTeX

$$$IsGLB\\{ y \\\\mid x \\\\le y \\\\wedge c.IsClosed y \\} (c x)$$$

Lean4

theorem closure_isGLB (x : α) : IsGLB {y | x ≤ y ∧ c.IsClosed y} (c x)
    where
  left _ := and_imp.mpr closure_min
  right _ h := h ⟨c.le_closure x, c.isClosed_closure x⟩

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