map_comp — Mathlib

English

Uniform continuous maps respect composition: Completion.map g ∘ Completion.map f = Completion.map (g ∘ f).

Русский

Порядок композиции сохранён: Completion.map g ∘ Completion.map f = Completion.map (g ∘ f).

LaTeX

$$$\\mathrm{UniformContinuous} g \\to \\mathrm{UniformContinuous} f \\to (\\mathrm{Completion.map} g) \\circ (\\mathrm{Completion.map} f) = \\mathrm{Completion.map} (g \\circ f)$$$

Lean4

theorem map_comp {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
    Completion.map g ∘ Completion.map f = Completion.map (g ∘ f) :=
  extension_map ((uniformContinuous_coe _).comp hg) hf

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