isUniformInducing_iff' — Mathlib

English

For any f, IsUniformInducing f is equivalent to UniformContinuous f and the comap of the product uniformity along f is ≤ the uniformity on domain.

Русский

Для f равномерно индуцирующее эквивалентно равномерной непрерывности и неравенству по комапу произведения по f.

LaTeX

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

Lean4

theorem isUniformInducing_iff' {f : α → β} :
    IsUniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α := by
  rw [isUniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]; rfl

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