toSubmodule_le_toSubmodule

Mathlib.Topology.Algebra.Module.ClosedSubmodule

URI: https://scilib.ai/kg/mathlib#ClosedSubmodule.toSubmodule_le_toSubmodule

English

For ClosedSubmodule s,t, the inequality of their toSubmodule is equivalent to the inequality of s and t.

Русский

Для подпмодулей s,t: s.toSubmodule ≤ t.toSubmodule эквивалентно s ≤ t.

LaTeX

$$$s.toSubmodule \leq t.toSubmodule \;\Leftrightarrow\; s \leq t.$$$

Lean4

@[simp, norm_cast]
theorem toSubmodule_le_toSubmodule {s t : ClosedSubmodule R M} : s.toSubmodule ≤ t.toSubmodule ↔ s ≤ t :=
  .rfl

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

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

Разделы

Аффилиация

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