English
The uniformity on α equals the lift by interior: 𝓤 α = (𝓤 α).lift' interior.
Русский
Униформность на α равна подъему через внутреннее (interior): 𝓤 α = (𝓤 α).lift' interior.
LaTeX
$$$\mathcal{U}(α) = (\mathcal{U}(α)).lift'\, interior$$$
Lean4
theorem uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
le_antisymm
(le_iInf₂ fun d hd => by
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
have : s ⊆ interior d :=
calc
s ⊆ t := hst
_ ⊆ interior d :=
ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
hs_comp ⟨x, h₁, y, h₂, h₃⟩
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this
simp [this])
fun _ hs => ((𝓤 α).lift' interior).sets_of_superset (mem_lift' hs) interior_subset
