toSubmodule_injective — Mathlib

English

Two LieSubalgebras are equal iff they have the same membership relation for every element of L.

Русский

Две подалгебры равны тогда, когда для каждого элемента x ∈ L верно x ∈ L' ⇔ x ∈ L''.

LaTeX

$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L]\ (L' L'' : \text{LieSubalgebra } R L),\ (\forall x, x \in L' \iff x \in L'') \Rightarrow L' = L''. $$$$

Lean4

theorem toSubmodule_injective : Function.Injective ((↑) : LieSubalgebra R L → Submodule R L) := fun L₁' L₂' h ↦
  by
  rw [SetLike.ext'_iff] at h
  rw [← coe_set_eq]
  exact h

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