comap_uniformity_le — Mathlib

English

Reiterates that AntilipschitzWith f implies the comap inequality of uniformities.

Русский

Повторное утверждение об антилипшицивости и сопряженной униформности.

LaTeX

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

Lean4

theorem comap_uniformity_le (hf : AntilipschitzWith K f) : (𝓤 β).comap (Prod.map f f) ≤ 𝓤 α :=
  by
  refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
  refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
  refine fun x hx => (hf x.1 x.2).trans_lt ?_
  rw [mul_comm, ← div_eq_mul_inv] at hx
  rw [mul_comm]
  exact ENNReal.mul_lt_of_lt_div hx

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