lieSpan_eq_bot_iff

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.lieSpan_eq_bot_iff

English

lieSpan(s) = ⊥ if and only if every m ∈ s is zero.

Русский

lieSpan(s) = ⊥ тогда и только тогда, когда каждый элемент s равен нулю.

LaTeX

$$lieSpan_{R,L}(s) = \\bot \\;\\iff\\; \\forall m\\in s, \\ m = 0$$

Lean4

theorem lieSpan_eq_bot_iff : lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = (0 : M) := by
  rw [_root_.eq_bot_iff, lieSpan_le, bot_coe, subset_singleton_iff]

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

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

Разделы

Аффилиация

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