instPartialOrder

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.instPartialOrder

Lean4

instance : PartialOrder (LieSubalgebra R L) :=
  { PartialOrder.lift ((↑) : LieSubalgebra R L → Set L) coe_injective with le := fun N N' ↦ ∀ ⦃x⦄, x ∈ N → x ∈ N' }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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