equivOfLe — Mathlib

English

There is a canonical Lie algebra isomorphism between K and its image in K' given by the inclusion when K ≤ K'.

Русский

Существует каноническое изоморфизм Ли между K и его образом в K' по включению при K ≤ K'.

LaTeX

$$K ≃_L⁅R⁆ (ofLe h)$$

Lean4

/-- Given nested Lie subalgebras `K ⊆ K'`, there is a natural equivalence from `K` to its image in
`K'`. -/
noncomputable def equivOfLe : K ≃ₗ⁅R⁆ ofLe h :=
  (inclusion h).equivRangeOfInjective (inclusion_injective h)

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