ωConjLieSubmodule_eq_top_iff — Mathlib

English

ωConjLieSubmodule N equals the top submodule if and only if N equals the top submodule.

Русский

ωConjLieSubmodule N совпадает с верхним подпространством тогда и только тогда, когда N совпадает с верхним подпространством.

LaTeX

$$$\\omegaConjLieSubmodule N = \\top \\iff N = \\top$$$

Lean4

@[simp]
theorem ωConjLieSubmodule_eq_top_iff : ωConjLieSubmodule N = ⊤ ↔ N = ⊤ :=
  by
  rw [← LieSubmodule.toSubmodule_eq_top]
  let e : Submodule R (b.support ⊕ ι → R) ≃o Submodule R (b.support ⊕ ι → R) :=
    Submodule.orderIsoMapComapOfBijective (ω b).toLin' (Involutive.bijective fun x ↦ by simp)
  change e.symm N = ⊤ ↔ _
  simp

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