iInf_comap_proj

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#Submodule.iInf_comap_proj

English

The infimum over all i of comap(proj_i, p_i) equals pi univ p.

Русский

Гиперинимика непрерывного проектора по всем i даёт pi Set.univ p.

LaTeX

$$$$\\bigwedge_i \\mathrm{comap}(\\mathrm{proj}_i, p_i) = \\pi(\\mathrm{Set.univ}, p).$$$$

Lean4

theorem iInf_comap_proj : ⨅ i, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi Set.univ p :=
  by
  ext x
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru