uniformity_eq_uniformity_closure — Mathlib

English

The uniformity on α is equal to the lift of the closure operator applied to the uniformity: 𝓤 α = (𝓤 α).lift' closure.

Русский

Униформность на α равна подъему операции замыкания примененной к самой униформности: 𝓤 α = (𝓤 α).lift' closure.

LaTeX

$$$\mathcal{U}(α) = (\mathcal{U}(α)).lift'\, closure$$$

Lean4

theorem uniformity_eq_uniformity_closure : 𝓤 α = (𝓤 α).lift' closure :=
  Eq.symm <| uniformity_hasBasis_closed.lift'_closure_eq_self fun _ => And.right

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