ι_π — Mathlib

English

For any b,c, the composite Pi.ι f b ≫ Pi.π f c equals if b=c then eqToHom (congrArg f h) else 0, i.e., equals the identity when indices match and zero otherwise.

Русский

Для любых b,c композит Pi.ι f b ≫ Pi.π f c равен, если b=c, то равен гомоморфизму-экв, иначе нулю.

LaTeX

$$$\Pi\!\iota_f(b) \;\circ\; \Pi\!\pi_f(c) = \begin{cases} \mathrm{eqToHom}(f,h) & \text{if } b=c \text{ with } h: b=c, \\ 0 & \text{otherwise}. \end{cases}$$$

Lean4

@[reassoc]
theorem ι_π (b c : β) : Pi.ι f b ≫ Pi.π f c = if h : b = c then eqToHom (congrArg f h) else 0 :=
  by
  split_ifs with h
  · subst h; simp
  · simp [Pi.ι_π_of_ne f h]

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