normalizeIsoApp_eq — Mathlib

English

For a fixed C and X in FreeMonoidalCategory, the normalization map commutes with the iso-app construction when passing along the isomorphism data n.as.

Русский

Нормализация совместима с конструкцией изоморфизма приложения, передаваемого через n.as.

LaTeX

$$$ \forall X \forall n, normalizeIsoApp C X n = normalizeIsoApp' C X n.as $$$

Lean4

theorem normalizeIsoApp_eq : ∀ (X : F C) (n : N C), normalizeIsoApp C X n = normalizeIsoApp' C X n.as
  | of _, _ => rfl
  | unit, _ => rfl
  | tensor X Y, n => by
    rw [normalizeIsoApp, normalizeIsoApp']
    rw [normalizeIsoApp_eq X n]
    rw [normalizeIsoApp_eq Y ⟨normalizeObj X n.as⟩]
    rfl

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