ext — Mathlib

English

For a functor F from C to Type, two elements of F.Elements are equal if their first components are equal and the second components agree via the functor map.

Русский

Для функторa F: C ⥤ Type утверждение EXT: два элемента F.Elements равны, если их первые компоненты равны и вторые компоненты совпадают под отображением F.map.

LaTeX

$$$\\forall {F : C \\to Type_w} \\; (x,y : F.Elements),\\; (x.fst = y.fst) \\land (F.map (eqToHom h1) x.snd = y.snd) \\Rightarrow x = y$$$

Lean4

theorem ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst = y.fst) (h₂ : F.map (eqToHom h₁) x.snd = y.snd) : x = y :=
  by
  cases x
  cases y
  cases h₁
  simp only [eqToHom_refl, FunctorToTypes.map_id_apply] at h₂
  simp [h₂]

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