map_uniformity_set_coe — Mathlib

English

The map of Prod.map on Subtype.val induces the equality map of uniformities: map (Prod.map (↑) (↑)) (𝓤 s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s).

Русский

Отображение Prod.map(↑,↑) применяется к 𝓤 s и равно 𝓤 α ∧ 𝓟 (s×s).

LaTeX

$$$$\\mathrm{map}(\\mathrm{Prod.map}(\\uparrow, \\uparrow))(\\mathcal{U}(s)) = \\mathcal{U}(\\alpha) \\sqcap \\mathcal{P}(s \\times\\, s).$$$$

Lean4

theorem map_uniformity_set_coe {s : Set α} [UniformSpace α] : map (Prod.map (↑) (↑)) (𝓤 s) = 𝓤 α ⊓ 𝓟 (s ×ˢ s) := by
  rw [uniformity_setCoe, map_comap, range_prodMap, Subtype.range_val]

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