of_f — Mathlib

English

There exists a finite witness i and y witnessing an equality with x in the direct limit.

Русский

Существует конечный свидетель i и y, доказывающий равенство x в пределе.

LaTeX

$$$\\exists i,\\exists y, x = \\mathrm{Quotient.mk}(\\dots)(\\mathrm{Sigma.mk}(f,i,y))$$$

Lean4

theorem of_f {i j : ι} {hij : i ≤ j} {x : G i} : of L ι G f j (f i j hij x) = of L ι G f i x :=
  by
  rw [of_apply, of_apply, Quotient.eq]
  refine Setoid.symm ⟨j, hij, refl j, ?_⟩
  simp only [DirectedSystem.map_self]

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