one_def — Mathlib

English

In a directed system, an element in the DirectLimit equals 1 if and only if its representative is eventually mapped to 1 at some stage of the system.

Русский

В направленной системе элемент в прямом пределе равен единице тогда и только тогда, когда его представитель в некотором шаге системы отображается в единицу.

LaTeX

$$$\\langle x, \\_ \\rangle = 1 \\iff \\exists i,h, f\\langle x,i,h\\rangle = 1$$$

Lean4

@[to_additive]
theorem one_def (i) : (1 : DirectLimit G f) = ⟦⟨i, 1⟩⟧ :=
  map₀_def _ _ (fun _ _ _ ↦ map_one _) _

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