extension_comp_coe — Mathlib

English

If f: Completion α → β is uniformly continuous and ↑ denotes the canonical coe from α to Completion α, then the extension of f composed with coe equals f; that is, Completion.extension (f ∘ (↑)) = f.

Русский

Если f: Completion α → β непрерывно по униформности и ↑ обозначает каноническое вложение α в Completion α, то продолжение f после вложения совпадает с f; то есть Completion.extension (f ∘ (↑)) = f.

LaTeX

$$$\\forall f : \\mathrm{Completion}(\\alpha) \\to \\beta\\, (\\mathrm{UniformContinuous} f) \\Rightarrow \\mathrm{Completion.extension} (f \\circ \\mathrm{coe}) = f$$$

Lean4

@[simp]
theorem extension_comp_coe {f : Completion α → β} (hf : UniformContinuous f) : Completion.extension (f ∘ (↑)) = f :=
  cPkg.extend_comp_coe hf

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