tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe

English

If F is locally uniformly convergent and g is a map with appropriate continuity, then the composition F∘g is locally uniformly convergent to f∘g with respect to p on the image of the domain.

Русский

Если локально-однородная сходимость для F и f, и g непрерывна, то композиция F∘g сходится локально равномерно к f∘g на соответствующем подмножестве.

LaTeX

$$$$\operatorname{TendstoLocallyUniformlyOn}\bigl(F\circ g, f\circ g, p, t\bigr) \leftarrow \operatorname{TendstoLocallyUniformlyOn}(F,f,p,s)$$$$

Lean4

theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe :
    TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p := by
  simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right];
  rfl

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