ext — Mathlib

English

If f,g: Completion α → Y are continuous and agree on α, then f=g.

Русский

Если f,g: Completion α → Y непрерывны и согласуются на α, то f=g.

LaTeX

$$$\\text{Continuous}(f)\\ \\&\\ \\text{Continuous}(g)\\ \\&\\ \\forall a:\\alpha,\\ f(\\mathrm{coe}'a)=g(\\mathrm{coe}'a)\\Rightarrow f=g$$$

Lean4

theorem ext {Y : Type*} [TopologicalSpace Y] [T2Space Y] {f g : Completion α → Y} (hf : Continuous f)
    (hg : Continuous g) (h : ∀ a : α, f a = g a) : f = g :=
  cPkg.funext hf hg h

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