comap_inf — Mathlib

English

The comap of the infimum of two uniform structures along f equals the infimum of the comaps along f.

Русский

Обратная связь инфимума двух равномерных структур по f равна инфимуму обратных образов по f этих структур.

LaTeX

$$(u_1 ⊓ u_2).comap f = u_1.comap f ⊓ u_2.comap f$$

Lean4

theorem comap_inf {α γ} {u₁ u₂ : UniformSpace γ} {f : α → γ} : (u₁ ⊓ u₂).comap f = u₁.comap f ⊓ u₂.comap f :=
  UniformSpace.ext Filter.comap_inf

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