neg_iInf

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

Negation commutes with arbitrary iInf: (-⨅ i, S i) = ⨅ i, (-S i).

Русский

Отрицание коммутирует iInf: (-⨅ i, S i) = ⨅ i, (-S i).

LaTeX

$$$(-\inf_i S_i) = \inf_i (-S_i)$$$

Lean4

@[simp]
theorem neg_iInf {ι : Sort*} (S : ι → Submodule R M) : (-⨅ i, S i) = ⨅ i, -S i :=
  (negOrderIso : Submodule R M ≃o Submodule R M).map_iInf _

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

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

Разделы

Аффилиация

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