inclusion_faithful — Mathlib

English

For any h: S ≤ T, the inclusion functor is faithful on arrows: distinct arrows remain distinct after applying the map.

Русский

Для включения h: S ≤ T функтор включения сохраняет различимость стрел: различные стрелки остаются различными под действием отображения.

LaTeX

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

Lean4

theorem inclusion_faithful {S T : Subgroupoid C} (h : S ≤ T) (s t : S.objs) :
    Function.Injective fun f : s ⟶ t => (inclusion h).map f := fun ⟨f, hf⟩ ⟨g, hg⟩ => by
  -- Porting note: was `...; simpa only [Subtype.mk_eq_mk] using id`
  dsimp only [inclusion]; rw [Subtype.mk_eq_mk, Subtype.mk_eq_mk]; exact id

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