inseparable_iff_uniformity — Mathlib

English

The uniformity on the quotient α ↦ SeparationQuotient α is the pushforward of 𝓤α along the map mk, i.e., comap of the quotient map equals the original uniformity.

Русский

Равномерность на факторпространстве α → SeparationQuotient α равна образованию по отображению mk, то есть равносильность равномерностей через комап и отображение mk.

LaTeX

$$$(\mathcal{U}(\ SeparationQuotient(α))) = (\mathcal{U}(α)).map (Prod.map mk mk)$$$

Lean4

theorem inseparable_iff_uniformity {β} {l : Filter β} [NeBot l] {f g : β → α} {a b : α} (ha : Tendsto f l (𝓝 a))
    (hb : Tendsto g l (𝓝 b)) : Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) :=
  by
  refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
  rw [inseparable_iff_clusterPt_uniformity]
  exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

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