English
In a directed system of sets (or groups) with a distinguished unit, an element [i,x] in the direct limit equals the unit if and only if there exist an index i and a stage h such that transporting x to i via the system maps yields 1 at that stage.
Русский
В направленной системе множеств (или групп) с обозначенной нейтральной единицей элемент \([i,x]\) в прямом пределе равен единице тогда и только тогда, когда существует индекс i и этап h, для которого перенос элемента x по системе даёт 1 на этом этапе.
LaTeX
$$$\bigl[ i, x \bigr] = 1 \iff \exists i,h, \, f\_{x,i,h}(x) = 1.$$$
Lean4
@[to_additive]
theorem exists_eq_one (x) : ⟦x⟧ = (1 : DirectLimit G f) ↔ ∃ i h, f x.1 i h x.2 = 1 :=
by
rw [one_def x.1, Quotient.eq]
exact ⟨fun ⟨i, h, _, eq⟩ ↦ ⟨i, h, eq.trans (map_one _)⟩, fun ⟨i, h, eq⟩ ↦ ⟨i, h, h, eq.trans (map_one _).symm⟩⟩
