map_unique — Mathlib

English

If f is uniformly continuous and g is any map with mk ∘ f = g ∘ mk, then map f = g on SeparationQuotient.

Русский

Если f равномерно непрерывно и существует g с mk ∘ f = g ∘ mk, то map f = g.

LaTeX

$$Theorem: map f = g if comm: mk ∘ f = g ∘ mk and hf is UniformContinuous f.$$

Lean4

theorem map_unique {f : α → β} (hf : UniformContinuous f) {g : SeparationQuotient α → SeparationQuotient β}
    (comm : mk ∘ f = g ∘ mk) : map f = g := by
  ext ⟨a⟩
  calc
    map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
    _ = g ⟦a⟧ := congr_fun comm a

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