comp_inv_app — Mathlib

English

Similarly, the inverse component of a composition is the identity on any open.

Русский

Аналогично, обратная компонентa композиции равна тождественному отображению на любом открытом

LaTeX

$$((comp f g ℱ).inv.app U) = 𝟙 _$$

Lean4

@[simp]
theorem comp_inv_app {X Y Z : TopCat.{w}} (f : X ⟶ Y) (g : Y ⟶ Z) (ℱ : X.Presheaf C) (U) :
    (comp f g ℱ).inv.app U = 𝟙 _ :=
  rfl

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