comap_inf_principal_range — Mathlib

English

Pullback along m distributes over infimum with a principal: comap m (g ⊓ 𝓟(range m)) = comap m g.

Русский

Обратное изображение по m распределяет по inf и по примитиву: comap m (g ⊓ 𝓟(range m)) = comap m g.

LaTeX

$$$ \\operatorname{comap}_m\\bigl( g \\;\\sqcap\\; \\mathcal{P}(\\operatorname{range}(m)) \\bigr) = \\operatorname{comap}_m g $$$

Lean4

theorem comap_inf_principal_range : comap m (g ⊓ 𝓟 (range m)) = comap m g := by simp

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