biInf_comap_proj

Mathlib.LinearAlgebra.Pi

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

English

The infimum over i ∈ I of comap(proj_i, p_i) equals pi I p.

Русский

Граниение по всем i ∈ I от comap(proj_i, p_i) равно pi I p.

LaTeX

$$$$\\bigwedge_{i\\in I} \\mathrm{comap}(\\mathrm{proj}_i, p_i) = \\pi I p.$$$$

Lean4

theorem biInf_comap_proj : ⨅ i ∈ I, comap (proj i : ((i : ι) → φ i) →ₗ[R] φ i) (p i) = pi I p :=
  by
  ext x
  simp

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

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

Разделы

Аффилиация

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