ext — Mathlib

English

In Kleisli categories, equality of morphisms is determined pointwise by their action on each element.

Русский

В Kleisli категории равенство морфизмов определяется по точкам (по заданию на каждом элементе).

LaTeX

$$$$\\forall m\\; [\\text{Monad } m] \\; (\\alpha,\\beta:\\mathrm{KleisliCat}\; m)\\; (f,g:\\alpha \\to \\beta)\\; (\\forall x, f x = g x) \\Rightarrow f = g.$$$$

Lean4

@[ext]
theorem ext {m} [Monad.{u, v} m] (α β : KleisliCat m) (f g : α ⟶ β) (h : ∀ x, f x = g x) : f = g :=
  funext h

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