uniformSpace_comap_id — Mathlib

English

The comap of the identity map is the identity uniform space: UniformSpace.comap id = id.

Русский

Обратное отображение по тождеству даёт то же самое униформное пространство: UniformSpace.comap id = id.

LaTeX

$$$\text{[simp]}\theorem uniformSpace_comap_id {α : Type*} : UniformSpace.comap (id : α → α) = id$$$

Lean4

@[simp]
theorem uniformSpace_comap_id {α : Type*} : UniformSpace.comap (id : α → α) = id :=
  by
  ext : 2
  rw [uniformity_comap, Prod.map_id, comap_id]

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