inclusion_injective — Mathlib

English

The inclusion map h is injective for any S ≤ T; distinct elements of S map to distinct elements of T.

Русский

Включение h инъективно: различные элементы S отображаются в разные элементы T.

LaTeX

$$$\\text{inclusion}_h\\;\\text{is injective}$$$

Lean4

theorem inclusion_injective {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) : Function.Injective (inclusion h) :=
  fun _ _ => Subtype.ext ∘ Subtype.mk.inj

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