ext — Mathlib

English

Two natural transformations of presheaves are equal if they agree on every open; extensional principle.

Русский

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

LaTeX

$$$ \\forall U, f.app U = g.app U \\Rightarrow f = g $$$

Lean4

@[ext]
theorem ext {X : TopCat} {P Q : Presheaf C X} {f g : P ⟶ Q} (w : ∀ U : Opens X, f.app (op U) = g.app (op U)) : f = g :=
  by
  apply NatTrans.ext
  ext U
  induction U with
  | _ U => ?_
  apply w

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