separationQuotient — Mathlib

English

The separation quotient of a space X with ultra-uniformity inherits ultra-uniformity.

Русский

Разделительная квартация (separation quotient) пространства X с ультра-равномерностью наследует ультра-равномерность.

LaTeX

$$$IsUltraUniformity\big(SeparationQuotient X\big)$$$

Lean4

instance separationQuotient [IsUltraUniformity X] : IsUltraUniformity (SeparationQuotient X) :=
  by
  have := IsUltraUniformity.hasBasis.map (Prod.map SeparationQuotient.mk (SeparationQuotient.mk (X := X)))
  rw [← SeparationQuotient.uniformity_eq] at this
  apply mk_of_hasBasis this
  · exact fun _ ⟨_, hU, _⟩ ↦ hU.image_prodMap _
  · refine fun U ⟨hU', _, hU⟩ ↦ ?_
    rintro x y z
    simp only [id_eq, Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq, forall_exists_index, and_imp]
    rintro a b hab rfl rfl c d hcd hc rfl
    have hbc : (b, c) ∈ U :=
      by
      rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity, Filter.mem_ker] at hc
      exact hc _ hU'
    exact ⟨a, d, hU (hU hab hbc) hcd, by simp, by simp⟩

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