zero_exact — Mathlib

English

In AddCommGroup.DirectLimit.of, if the image of x is zero, then x is sent to zero by some later transition map in the directed system.

Русский

В AddCommGroup.DirectLimit.of, если образ x = 0, тогда существует переходная карта позднее, которая отправляет x в ноль.

LaTeX

$$$\exists j,hij:\; f_{i,j}^{h}(x)=0$ given $\text{of}(i,x)=0$$$

Lean4

/-- A component that corresponds to zero in the direct limit is already zero in some
bigger module in the directed system. -/
theorem zero_exact [IsDirected ι (· ≤ ·)] [DirectedSystem G fun i j h ↦ f i j h] (i x) (h : of G f i x = 0) :
    ∃ j hij, f i j hij x = 0 :=
  Module.DirectLimit.of.zero_exact h

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