English
The second equality expresses the compatibility of the two realizations of the direct limit equivalence with respect to lift and of.
Русский
Вторая равенство выражает совместимость двух реализаций эквивалентности прямого предела по отношению к взводу и вложению.
LaTeX
$$$\\text{equiv}_{2} = \\text{eq}_2$$$
Lean4
/-- Every element of the direct limit corresponds to some element in
some component of the directed system. -/
theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f) : ∃ i x, of R ι G f i x = z :=
Nonempty.elim (by infer_instance) fun ind : ι ↦
Quotient.inductionOn' z fun z ↦
DirectSum.induction_on z ⟨ind, 0, LinearMap.map_zero _⟩ (fun i x ↦ ⟨i, x, rfl⟩) fun p q ⟨i, x, ihx⟩ ⟨j, y, ihy⟩ ↦
let ⟨k, hik, hjk⟩ := exists_ge_ge i j
⟨k, f i k hik x + f j k hjk y, by
rw [LinearMap.map_add, of_f, of_f, ihx, ihy]
rfl⟩
