instEpiFπTruncGE — Mathlib

English

Duplicate entry asserting epi for πTruncGE components.

Русский

Дублирующее утверждение, что компоненты πTruncGE являются эпиморфизмами.

LaTeX

$$$\forall i',\ Epi((K.πTruncGE e).f i')$$$

Lean4

instance (i' : ι') : Epi ((K.πTruncGE e).f i') :=
  by
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    dsimp [πTruncGE]
    rw [e.epi_liftExtend_f_iff _ _ hi]
    infer_instance
  · apply (isZero_extend_X _ _ _ (by simpa using hi')).epi

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