lie_le_inf

Mathlib.Algebra.Lie.IdealOperations

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

English

The bracket [I,J] is contained in the infimum I ⊓ J of I and J, i.e., [I,J] ≤ I ∩ J.

Русский

Скобка [I,J] содержится в пересечении I и J: [I,J] ≤ I ∩ J.

LaTeX

$$$$ [I,J] \le I \cap J. $$$$

Lean4

theorem lie_le_inf : ⁅I, J⁆ ≤ I ⊓ J := by rw [le_inf_iff]; exact ⟨lie_le_left I J, lie_le_right J I⟩

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

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

Разделы

Аффилиация

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