comap_iInf — Mathlib

English

The comap of the infimum over an index set commutes with taking infimum after pulling back along f: (⨅ i, u_i).comap f = ⨅ i, (u_i).comap f.

Русский

Обратный образ инфимума по индексу коммутирует с инфимумом после обратного образа: (⨅ i, u_i).comap f = ⨅ i, (u_i).comap f.

LaTeX

$$(\\inf_i u_i).comap f = \\inf_i (u_i.comap f)$$

Lean4

theorem comap_iInf {ι α γ} {u : ι → UniformSpace γ} {f : α → γ} : (⨅ i, u i).comap f = ⨅ i, (u i).comap f :=
  by
  ext : 1
  simp [uniformity_comap, iInf_uniformity]

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