uniformContinuous_iff — Mathlib

English

Given g is IsUniformInducing, UniformContinuous f iff UniformContinuous (g ∘ f).

Русский

Пусть g − IsUniformInducing, тогда UniformContinuous f эквивалентно UniformContinuous (g ∘ f).

LaTeX

$$$UniformContinuous f \\iff UniformContinuous (g \\circ f)$$$

Lean4

theorem uniformContinuous_iff {f : α → β} {g : β → γ} (hg : IsUniformInducing g) :
    UniformContinuous f ↔ UniformContinuous (g ∘ f) :=
  by
  dsimp only [UniformContinuous, Tendsto]
  simp only [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map, Function.comp_def]

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