ucs_mono

Mathlib.Algebra.Lie.Nilpotent

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

← MathLib Explorer

English

If N1 ≤ N2 then N1.ucs k ≤ N2.ucs k for any k.

Русский

Если N1 ⊆ N2, то N1.ucs k ⊆ N2.ucs k для любого k.

LaTeX

$$$\\forall k, \\, N_1 \\le N_2 \\Rightarrow N_1.ucs k \\le N_2.ucs k.$$$

Lean4

@[gcongr, mono]
theorem ucs_mono (k : ℕ) (h : N₁ ≤ N₂) : N₁.ucs k ≤ N₂.ucs k := by
  induction k with
  | zero => simpa
  | succ k ih =>
    simp only [ucs_succ]
    gcongr

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

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

Разделы

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

Аффилиация

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