ext' — Mathlib

English

A variant of ext: if f,g continuous and agree on α, then f=g on all of Completion α.

Русский

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

LaTeX

$$$\\forall a:\\alpha,\\ f a = g 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) (a : Completion α) : f a = g a :=
  congr_fun (ext hf hg h) a

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