uniformContinuousOn_iff — Mathlib

English

If g is IsUniformInducing, UniformContinuousOn f on S iff UniformContinuousOn (g ∘ f) on S.

Русский

Если g — IsUniformInducing, то UniformContinuousOn f на S эквивалентно UniformContinuousOn (g ∘ f) на S.

LaTeX

$$$UniformContinuousOn f S \\iff UniformContinuousOn (g \\circ f) S$$$

Lean4

theorem uniformContinuousOn_iff {f : α → β} {g : β → γ} {S : Set α} (hg : IsUniformInducing g) :
    UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S :=
  by
  dsimp only [UniformContinuousOn, Tendsto]
  rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, comp_def, comp_def]

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