inclusion_injective — Mathlib

English

If I1 and I2 are Lie ideals of a Lie algebra L with I1 ≤ I2, then the natural inclusion map from I1 to I2 is injective.

Русский

Если I1 и I2 — лие-идеалы L и I1 ⊆ I2, то естественное включение I1 в I2 является инъективным.

LaTeX

$$$\iota_h: I_1 \to I_2 \quad\text{является инъективным},$ то есть $\iota_h(x)=\iota_h(y) \Rightarrow x=y$ для всех $x,y \in I_1$.$$

Lean4

theorem inclusion_injective {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) : Function.Injective (inclusion h) := fun x y ↦ by
  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

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