inv_whiskerRight — Mathlib

English

The inverse of the whiskering of an isomorphism by φ equals the whiskering of the inverse by φ: inv(η ▷ φ) = inv η ▷ φ.

Русский

Обратный whiskerRight изоморфизма по φ равен whiskerRight обратного изоморфизма по φ: inv(η ▷ φ) = inv η ▷ φ.

LaTeX

$$$\\operatorname{inv}(\\eta \\!\\rhd\\! \\phi) = \\operatorname{inv}\\eta \\!\\rhd\\! \\phi$$$

Lean4

theorem inv_whiskerRight : inv (η ▷ φ) = inv η ▷ φ :=
  by
  apply IsIso.inv_eq_of_hom_inv_id
  simp [← comp_whiskerRight]

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