neg_sup

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

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

Русский

Отрицание коммутирует произвольное объединение: -⨆i S(i) = ⨆i (-S(i)).

LaTeX

$$$-\bigvee_{i} S(i) = \bigvee_{i} (-S(i))$$$

Lean4

@[simp]
theorem neg_sup (S T : Submodule R M) : -(S ⊔ T) = -S ⊔ -T :=
  (negOrderIso : Submodule R M ≃o Submodule R M).map_sup S T

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

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

Разделы

Аффилиация

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