of_comp — Mathlib

English

If f and g are uniformly continuous and g∘f is IsUniformInducing, then f is IsUniformInducing.

Русский

Если f и g равномерно непрерывны и g∘f — IsUniformInducing, тогда f — IsUniformInducing.

LaTeX

$$$IsUniformInducing f$$$

Lean4

theorem of_comp {f : α → β} {g : β → γ} (hf : UniformContinuous f) (hg : UniformContinuous g)
    (hgf : IsUniformInducing (g ∘ f)) : IsUniformInducing f :=
  by
  refine ⟨le_antisymm ?_ hf.le_comap⟩
  rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
  exact comap_mono hg.le_comap

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