comap_map_mk_uniformity — Mathlib

English

For a T0-space β and f: α → β, lift' f applied to the class mk a equals f a; i.e., lifting through the quotient preserves evaluation on canonical representatives.

Русский

Для T0-пространства β и отображения f: α → β, lift' f на каноническом представительстве равен f a.

LaTeX

$$$\text{lift'} f (\mathrm{mk}\ a) = f\ a$$$

Lean4

theorem comap_map_mk_uniformity : comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α :=
  by
  refine le_antisymm ?_ le_comap_map
  refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_
  refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩
  simp only [Prod.map, Prod.ext_iff, mk_eq_mk] at hxy
  exact ((hxy.1.prod hxy.2).mem_open_iff hU.2).1 hyU

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