English
If two elements x,y ∈ G_i have the same image in the direct limit, i.e. of i x = of i y, then there exists a stage j ≥ i and a transition map f_i_j(h) such that f_i_j(h)(x) = f_i_j(h)(y) in G_j.
Русский
Если элементы x,y ∈ G_i имеют одинаковое изображение в прямом пределе, то существует этап j ≥ i и переходная карта f_i_j(h), такая что f_i_j(h)(x) = f_i_j(h)(y) в G_j.
LaTeX
$$$\forall i\,x,y\in G_i,\; \text{of}(i,x)=\text{of}(i,y) \Rightarrow \exists j\; hij,\; f_{i,j}(h)(x)=f_{i,j}(h)(y)$$$
Lean4
theorem exists_eq_of_of_eq {i x y} (h : of R ι G f i x = of R ι G f i y) : ∃ j hij, f i j hij x = f i j hij y :=
by
have := Nonempty.intro i
apply_fun linearEquiv _ _ at h
simp_rw [linearEquiv_of] at h
have ⟨j, h⟩ := Quotient.exact h
exact ⟨j, h.1, h.2.2⟩
