exact_of_comp_of_mem_range — Mathlib

English

If g∘f = 0 and every zero of g lies in range f, then f,g are exact.

Русский

Если g∘f = 0 и каждое нулевое значение g лежит в образе f, тогда точность выполняется.

LaTeX

$$$(g\\circ f)=0 \\land \\forall x,\\ g(x)=0 \\Rightarrow x \\in \\mathrm{range}(f) \\Rightarrow \\mathrm{Exact}(f,g)$$$

Lean4

theorem exact_of_comp_of_mem_range (h1 : g.comp f = 0) (h2 : ∀ x, g x = 0 → x ∈ range f) : Exact f g :=
  exact_of_comp_eq_zero_of_ker_le_range h1 h2

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