replaceTopology — Mathlib

English

Replace the topology in a UniformSpace by a propositionally equal one.

Русский

Заменить топологию в UniformSpace на равносильную по смыслу.

LaTeX

$$$\\text{replaceTopology }(h) : UniformSpace α$$$

Lean4

/-- Replace topology in a `UniformSpace` instance with a propositionally (but possibly not
definitionally) equal one. -/
abbrev replaceTopology {α : Type*} [i : TopologicalSpace α] (u : UniformSpace α) (h : i = u.toTopologicalSpace) :
    UniformSpace α where
  __ := u
  toTopologicalSpace := i
  nhds_eq_comap_uniformity x := by rw [h, u.nhds_eq_comap_uniformity]

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