appIso_hom' — Mathlib

English

A variant of the previous expression states the same equality using a shifted formulation: (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).ge).op.

Русский

Вариант предыдущего выражения формулирует то же равенство через немного перенесённую форму: (f.appIso U).hom = f.app (f''ᵁ U) ∘ X.presheaf.map (eqToHom (preimage_image_eq f U).ge).op.

LaTeX

$$$$ (f.appIso U).hom = f.app (f''^\!U) \circ X.presheaf.map (eqToHom (preimage_image_eq f U).ge).op $$$$

Lean4

theorem appIso_hom' (U) : (f.appIso U).hom = f.appLE (f ''ᵁ U) U (preimage_image_eq f U).ge :=
  f.appIso_hom U

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