piCongrRight_refl — Mathlib

English

Composition of piCongrRight corresponds pointwise to composition of the component equivalences.

Русский

Составление piCongrRight соответствует по точкам композиции компонентных эквивалентностей.

LaTeX

$$$$ (\\pi\\mathrm{CongrRight} e)\\;\\mathrm{trans}\\; (\\pi\\mathrm{CongrRight} f) = \\pi\\mathrm{CongrRight} (i \\mapsto e_i \\circ f_i). $$$$

Lean4

@[simp]
theorem piCongrRight_refl : (piCongrRight fun j => refl R (φ j)) = refl _ _ :=
  rfl

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