isUniformInducing_comp_iff — Mathlib

English

Equivalence between isUniformInducing and a pair (UniformContinuous, comap bound).

Русский

Эквивалентность: IsUniformInducing f ⇔ UniformContinuous f и дополнительные неравенства.

LaTeX

$$$IsUniformInducing f \\iff UniformContinuous f \\land comap (Prod.map f f) (\\mathcal{U} β) \\le \\mathcal{U} α$$$

Lean4

protected theorem isUniformInducing_comp_iff {f : α → β} {g : β → γ} (hg : IsUniformInducing g) :
    IsUniformInducing (g ∘ f) ↔ IsUniformInducing f := by
  simp only [isUniformInducing_iff, ← hg.comap_uniformity, comap_comap, Function.comp_def]

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