neg_iSup

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

Negation commutes with arbitrary iSup: (-⨆ i, S i) = ⨆ i, (-S i).

Русский

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

LaTeX

$$$(-\sup_i S_i) = \sup_i (-S_i)$$$

Lean4

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

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

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

Разделы

Аффилиация

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