isoOfIso — Mathlib

English

There is a natural isomorphism between piOpens of F and piOpens of G given an iso F ≅ G.

Русский

Существует естественный изоморфизм между piOpens(F) и piOpens(G) при изоморфизме F ≅ G.

LaTeX

$$$\piOpens F U \cong \piOpens G U$$$

Lean4

/-- Isomorphic presheaves have isomorphic `piInters` for any cover `U`. -/
@[simp]
def isoOfIso (α : F ≅ G) : piInters F U ≅ piInters.{v'} G U :=
  Pi.mapIso fun _ => α.app _

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