isUniformInducing_extend — Mathlib

English

Let i: α → β be a map that is both dense-inducing and uniform-inducing, and let f: α → γ be uniform-inducing. Then the extension of f along i is uniform-inducing.

Русский

Пусть i: α → β является отображением с плотным индукционирующим свойством и равномерно-индуцирующим свойством, и пусть f: α → γ равномерно индуцировано. Тогда продолжение f вдоль i является равномерно индуцирующим.

LaTeX

$$$$\text{If } \text{hid} : \text{IsDenseInducing}(i),\ hi : \text{IsUniformInducing}(i),\ h : \text{IsUniformInducing}(f)\text{ then } \text{IsUniformInducing}(\text{hid}.extend f). $$$$

Lean4

theorem isUniformInducing_extend {γ : Type*} [UniformSpace γ] [CompleteSpace β] [CompleteSpace γ] {i : α → β}
    {f : α → γ} (hid : IsDenseInducing i) (hi : IsUniformInducing i) (h : IsUniformInducing f) :
    IsUniformInducing (hid.extend f) := by
  let sf := SeparationQuotient.mk ∘ f
  have : CompleteSpace (closure (range sf)) := isClosed_closure.isComplete.completeSpace_coe
  let ff : α → closure (range sf) := inclusion subset_closure ∘ rangeFactorization sf
  have hgu : IsUniformInducing ff :=
    (isUniformEmbedding_set_inclusion subset_closure).isUniformInducing.comp
      (SeparationQuotient.isUniformInducing_mk.comp h).rangeFactorization
  have hgd : DenseRange ff :=
    ((denseRange_inclusion_iff subset_closure).2 subset_rfl).comp rangeFactorization_surjective.denseRange
      (continuous_inclusion subset_closure)
  have hg : IsDenseInducing ff := hgu.isDenseInducing hgd
  let fwd := hid.extend ff
  have hfwd : UniformContinuous fwd := uniformContinuous_uniformly_extend hi hid.dense hgu.uniformContinuous
  have hg' : UniformContinuous (hg.extend i) := uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous
  have key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk :=
    by
    ext x
    induction x using isClosed_property hid.dense
    ·
      exact
        isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous) SeparationQuotient.continuous_mk
    ·
      simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous] using
        hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt
  have hfu : IsUniformInducing fwd :=
    by
    refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
    rw [Function.comp_assoc, key]
    exact SeparationQuotient.isUniformInducing_mk
  have hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f)) :=
    by
    refine
      ((SeparationQuotient.continuous_mk.comp
                (uniformContinuous_uniformly_extend hi hid.dense
                    h.uniformContinuous).continuous).range_subset_closure_image_dense
            hid.dense).trans
        (closure_mono (subset_of_eq ?_))
    rw [← range_comp]
    apply congrArg range
    funext x
    simpa using (hid.inseparable_extend h.uniformContinuous.continuous.continuousAt)
  suffices Subtype.val ∘ fwd = SeparationQuotient.mk ∘ hid.extend f
    by
    rw [← SeparationQuotient.isUniformInducing_mk.isUniformInducing_comp_iff, ← this]
    exact (isUniformInducing_val _).comp hfu
  rw [← coe_comp_rangeFactorization (SeparationQuotient.mk ∘ hid.extend f), ← val_comp_inclusion hrr,
    Function.comp_assoc, Subtype.val_injective.comp_left.eq_iff]
  refine hid.extend_unique ?_ ?_
  · simp [ff, hid.inseparable_extend h.uniformContinuous.continuous.continuousAt, sf]
  ·
    exact
      (continuous_inclusion hrr).comp
        (SeparationQuotient.continuous_mk.comp
            (uniformContinuous_uniformly_extend hi hid.dense h.uniformContinuous).continuous).rangeFactorization

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