mem_map_submodule — Mathlib

English

For a LieEquiv e : L ≃ₗ⁅R⁆ L₂ and K ⊆ L, the map of K under e corresponds to the Submodule map of K in L.

Русский

Для отображения-равновесия e: L ≃ L₂ носитель K соответствует Submodule.map K в L₂.

LaTeX

$$$$\forall {R} {L} {L_2} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L]\ (K : \text{LieSubalgebra } R L) (e : L ≃ₗ⁅R⁆ L_2) (x : L_2),\ x \in K.map e \iff x \in (K : \text{Submodule } R L).map (e : L \to L_2). $$$$

Lean4

theorem mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (x : L₂) :
    x ∈ K.map (e : L →ₗ⁅R⁆ L₂) ↔ x ∈ (K : Submodule R L).map (e : L →ₗ[R] L₂) :=
  Iff.rfl

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