hom_ext — Mathlib

English

Two morphisms between truncated simplicial sets are equal if and only if their components at every level are equal.

Русский

Два морфизма между усечёнными симпликсальными множествами равны тогда и только тогда, когда их компоненты на каждом уровне равны.

LaTeX

$$$\forall X,Y\,(f,g: X \to Y),\; (\forall n,\; f_{n} = g_{n}) \Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {n : ℕ} {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
  NatTrans.ext (funext w)

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