of_comp_of_mem_range — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem of_comp_of_mem_range [Zero P] (h1 : g ∘ f = 0) (h2 : ∀ x, g x = 0 → x ∈ Set.range f) : Exact f g := fun y =>
  Iff.intro (h2 y) <| Exists.rec ((forall_apply_eq_imp_iff (p := (g · = 0))).mpr (congrFun h1) y)

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