compare_comp_eq_compare — Mathlib

English

Under continuity assumptions, the extension of the composition equals the composition of extensions.

Русский

При непрерывности выполняется равенство продолжения композиции и композиции продолжений.

LaTeX

$$$ (cont_f) \to (∀ a, Tendsto f...) \Rightarrow (IsDenseInducing.extend f) \circ pkg.compare pkg = pkg'.isDenseInducing.extend f $$$

Lean4

theorem compare_comp_eq_compare (γ : Type uγ) [TopologicalSpace γ] [T3Space γ] {f : α → γ} (cont_f : Continuous f) :
    letI := pkg.uniformStruct.toTopologicalSpace
    letI := pkg'.uniformStruct.toTopologicalSpace
    (∀ a : pkg.space, Filter.Tendsto f (Filter.comap pkg.coe (𝓝 a)) (𝓝 ((pkg.isDenseInducing.extend f) a))) →
      pkg.isDenseInducing.extend f ∘ pkg'.compare pkg = pkg'.isDenseInducing.extend f :=
  by
  let _ := pkg'.uniformStruct
  let _ := pkg.uniformStruct
  intro h
  have (x : α) : (pkg.isDenseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
    simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]
  apply
    (IsDenseInducing.extend_unique (AbstractCompletion.isDenseInducing _) this
        (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous)).symm
  apply IsDenseInducing.continuous_extend
  exact fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩

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