extend_comp_coe — Mathlib

English

For every uniformly continuous function f on hatα, the extension of the composition f ∘ ι equals f on hatα.

Русский

Для любой равномерно непрерывной функции f на hatα продолжение f ∘ ι совпадает с f на hatα.

LaTeX

$$$ (hf: UniformContinuous\, f) \\to pkg.extend (f \circ ι) = f $$$

Lean4

@[simp]
theorem extend_comp_coe {f : hatα → β} (hf : UniformContinuous f) : pkg.extend (f ∘ ι) = f :=
  funext fun x =>
    pkg.induction_on x (isClosed_eq pkg.continuous_extend hf.continuous) fun y =>
      pkg.extend_coe (hf.comp <| pkg.uniformContinuous_coe) y

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