map_comp — Mathlib

English

Uniformly continuous maps compose: map g after map f equals map (g ∘ f).

Русский

Сопоставления образуют композицию: map g ∘ map f = map (g ∘ f).

LaTeX

$$$ UniformContinuous g \to UniformContinuous f \to Eq (Function.comp (pkg'.map pkg'' g) (pkg.map pkg' f)) (pkg.map pkg'' (g \circ f)) $$$

Lean4

theorem map_comp {g : β → γ} {f : α → β} (hg : UniformContinuous g) (hf : UniformContinuous f) :
    pkg'.map pkg'' g ∘ pkg.map pkg' f = pkg.map pkg'' (g ∘ f) :=
  pkg.extend_map pkg' (pkg''.uniformContinuous_coe.comp hg) hf

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