trivial_iff_le_maximal_trivial — Mathlib

English

A LieModuleEquiv e induces a LieModuleEquiv between the maximal trivial submodules of M and N; the operation preserves brackets and sums.

Русский

Ли-эквивалент e индуцирует эквивалентность между максимальными тривиальными подмодулями M и N; операции сохраняют скобки и суммы.

LaTeX

$$$\\maxTrivEquiv\\;e: \\maxTrivSubmodule R L M \\simeq_{\\text{Lie}} \\maxTrivSubmodule R L N$ and preserves structure.$$

Lean4

theorem trivial_iff_le_maximal_trivial (N : LieSubmodule R L M) : IsTrivial L N ↔ N ≤ maxTrivSubmodule R L M :=
  ⟨fun h m hm x => IsTrivial.casesOn h fun h => Subtype.ext_iff.mp (h x ⟨m, hm⟩), fun h =>
    { trivial := fun x m => Subtype.ext (h m.2 x) }⟩

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