uSwitchEquiv_naturality — Mathlib

English

Naturality of uSwitchEquiv: for morphisms f, and element x, f(X.uSwitchEquiv(x)) = Y.uSwitchEquiv(uSwitch.map(f)(x)).

Русский

Естественность uSwitchEquiv: для отображения f и элемента x верно f(X.uSwitchEquiv(x)) = Y.uSwitchEquiv(uSwitch.map(f)(x)).

LaTeX

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

Lean4

theorem uSwitchEquiv_naturality {X Y : FintypeCat.{u}} (f : X ⟶ Y) (x : uSwitch.{u, v}.obj X) :
    f (X.uSwitchEquiv x) = Y.uSwitchEquiv (uSwitch.map f x) := by
  simp only [uSwitch, uSwitchEquiv, Equiv.trans_apply, Equiv.ulift_apply, Equiv.symm_apply_apply]

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