ext' — Mathlib

English

Morphisms of monads are equal if their underlying natural transformation components agree.

Русский

Морфизмы монад равны, если их подлежащие компоненты натуральных преобразований согласованы.

LaTeX

$$$\\\\forall {T_1 T_2 : \\text{Monad } C}\\\\ (f,g : T_1 \\to T_2) \\\\[ h : f.app = g.app \\\\\\to f = g$$$

Lean4

@[ext]
theorem ext' {T₁ T₂ : Monad C} (f g : T₁ ⟶ T₂) (h : f.app = g.app) : f = g :=
  MonadHom.ext h

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