English
For complete γ and T0, with f: β → γ and g: α → β uniformly continuous, the extension distributes over map: Extension f ∘ Map g = Extension (f ∘ g).
Русский
Для полного γ и T0, при непрерывности f: β → γ и g: α → β по униформности, продолжение распределяет композицию: Extension f ∘ Map g = Extension (f ∘ g).
LaTeX
$$$[\\text{CompleteSpace } \\gamma] \\to [T0Space \\gamma] \\\\ \\mathrm{Completion.extension} f \\circ \\mathrm{Completion.map} g = \\mathrm{Completion.extension} (f \\circ g)$$$
Lean4
theorem extension_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β} (hf : UniformContinuous f)
(hg : UniformContinuous g) : Completion.extension f ∘ Completion.map g = Completion.extension (f ∘ g) :=
Completion.ext (continuous_extension.comp continuous_map) continuous_extension <| by
simp [hf, hg, hf.comp hg, map_coe, extension_coe]
