English
If hf and hg are uniform continuous, then the extension commutes with map, i.e., extend f after map g equals extend (f ∘ g).
Русский
Если hf и hg равномерно непрерывны, то продолжение после отображения совпадает с продолжением композиции: extend f ∘ map g = extend (f ∘ g).
LaTeX
$$$ (hf: UniformContinuous f) \to (hg: UniformContinuous g) \to pkg'.extend f \circ map g = pkg.extend (f \circ g) $$$
Lean4
theorem extend_map [CompleteSpace γ] [T0Space γ] {f : β → γ} {g : α → β} (hf : UniformContinuous f)
(hg : UniformContinuous g) : pkg'.extend f ∘ map g = pkg.extend (f ∘ g) :=
pkg.funext (pkg'.continuous_extend.comp (pkg.continuous_map pkg' _)) pkg.continuous_extend fun a =>
by
rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
rfl
