pi_empty

Mathlib.LinearAlgebra.Pi

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

English

If every φ(i) is the whole space, then the pi of I with top submodules is still the top submodule.

Русский

Если каждая φ(i) равна всему пространству, то π(I, ⊤) равно ⊤.

LaTeX

$$$$\\pi(I, (\\top)) = \\top.$$$$

Lean4

@[simp]
theorem pi_empty (p : (i : ι) → Submodule R (φ i)) : pi ∅ p = ⊤ :=
  SetLike.coe_injective <| Set.empty_pi _

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

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

Разделы

Аффилиация

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