div₀_def — Mathlib

English

In a directed system with a multiplicative-like structure, taking representatives at a fixed index i and dividing by another element at the same index corresponds to taking the representative at the same index of the division x/y within the colimit.

Русский

В направленной системе, имеющей подобную структуру умножения, деление по представителям на фиксированном индексе i соответствует представителю на том же индексе элемента x/y в пределе.

LaTeX

$$$\forall i:\, ι,\, x,y:\, G(i),\; [i,x]\,[i,y]^{-1} = [i, x/y].$$$

Lean4

theorem div₀_def (i x y) : ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = (⟦⟨i, x / y⟩⟧ : DirectLimit G f) :=
  map₂_def ..

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