neg_le_neg

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

-S ≤ -T iff S ≤ T

Русский

-S ≤ -T тогда и только тогда, когда S ≤ T

LaTeX

$$$-S \le -T \iff S \le T$$$

Lean4

@[simp]
theorem neg_le_neg (S T : Submodule R M) : -S ≤ -T ↔ S ≤ T :=
  SetLike.coe_subset_coe.symm.trans Set.neg_subset_neg

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

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

Разделы

Аффилиация

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