CC_comp_zero — Mathlib

English

For all y, the composed map через πs C o evaluated at y yields zero.

Русский

Для всех y композиция через πs C o, применённая к y, равна нулю.

LaTeX

$$∀ y, (Linear_CC' C hsC ho) ((πs C o) y) = 0$$

Lean4

theorem CC_comp_zero : ∀ y, (Linear_CC' C hsC ho) ((πs C o) y) = 0 :=
  by
  intro y
  ext x
  dsimp [Linear_CC', Linear_CC'₀, Linear_CC'₁, LocallyConstant.sub_apply]
  simp only [sub_eq_zero]
  congr 1
  ext i
  dsimp [CC'₀, CC'₁, ProjRestrict, Proj]
  apply if_ctx_congr Iff.rfl _ (fun _ ↦ rfl)
  simp only [SwapTrue, ite_eq_right_iff]
  intro h₁ h₂
  exact (h₁.ne h₂).elim

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