uSwitchEquiv_symm_naturality — Mathlib

English

Naturality for the inverse side: uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x).

Русский

Естественность для обратной стороны: uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x).

LaTeX

$$$uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x)$$$

Lean4

theorem uSwitchEquiv_symm_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y) (x : X) :
    uSwitch.map f (X.uSwitchEquiv.symm x) = Y.uSwitchEquiv.symm (f x) := by
  rw [← Equiv.apply_eq_iff_eq_symm_apply, ← uSwitchEquiv_naturality f, Equiv.apply_symm_apply]

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