instInfSetUniformSpace — Mathlib

English

The uniformity on the top space equals the top filter: 𝓤[(⊤)].

Русский

Униформность верхнего пространства равна верхнему фильтру: 𝓤[(⊤)].

LaTeX

$$$𝓤[(⊤ : UniformSpace α)] = \top$$$

Lean4

instance : InfSet (UniformSpace α) :=
  ⟨fun s =>
    UniformSpace.ofCore
      { uniformity := ⨅ u ∈ s, 𝓤[u]
        refl := le_iInf fun u => le_iInf fun _ => u.toCore.refl
        symm := le_iInf₂ fun u hu => le_trans (map_mono <| iInf_le_of_le _ <| iInf_le _ hu) u.symm
        comp := le_iInf₂ fun u hu => le_trans (lift'_mono (iInf_le_of_le _ <| iInf_le _ hu) <| le_rfl) u.comp }⟩

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