exact_iff_degreewise_exact — Mathlib

English

Equivalent formulation that the degreewise exactness characterizes the overall exactness.

Русский

Эквивалентная формулировка, что точность по степеням характеризует общую точность.

LaTeX

$$$S.Exact \\iff \\forall i, (S.map (eval C c i)).Exact$$$

Lean4

theorem exact_iff_degreewise_exact : S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact :=
  by
  constructor
  · intro hS i
    exact hS.map (eval C c i)
  · exact exact_of_degreewise_exact S

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