ext — Mathlib

English

Two Oplax transformations between the same pair of Oplax functors are equal if they have identical components at every object.

Русский

Две преобразования Oplax между теми же самыми Oplax-функтороми равны, если их компоненты совпадают на каждом объекте.

LaTeX

$$$$ \\forall \\ F,G,\\alpha,\\beta,\\ m,n: \\alpha \\to \\beta,\\; (\\forall b, m\\app b = n\\app b) \\implies m=n. $$$$

Lean4

@[ext]
theorem ext {F G : OplaxFunctor B C} {α β : F ⟶ G} {m n : α ⟶ β} (w : ∀ b, m.app b = n.app b) : m = n :=
  by
  apply Modification.ext
  ext
  apply w

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