inclusion_inj_on_objects — Mathlib

English

If two objects in S map to the same object in T under inclusion, then the original objects are equal.

Русский

Если два объекта в S отображаются в один и тот же объект в T через включение, то исходные объекты равны.

LaTeX

$$h : S ≤ T → Function.Injective (inclusion h).obj$$

Lean4

theorem inclusion_inj_on_objects {S T : Subgroupoid C} (h : S ≤ T) : Function.Injective (inclusion h).obj :=
  fun ⟨s, hs⟩ ⟨t, ht⟩ => by simpa only [inclusion, Subtype.mk_eq_mk] using id

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