intCast_def — Mathlib

English

The embedding of NNrat into the directed limit is given by mapping q to the class ⟦⟨i,q⟩⟧ for any index i; this extends the idea of nat casts to NNrat.

Русский

В пределе прямой предел отображает NNrat через элемент ⟦⟨i,q⟩⟧ для любого индекса i.

LaTeX

$$$ (q : DirectLimit G f) = \overline{\langle i, q \rangle} $$$

Lean4

theorem intCast_def [∀ i j h, OneHomClass (T h) (G i) (G j)] (n : ℤ) (i) : (n : DirectLimit G f) = ⟦⟨i, n⟩⟧ :=
  map₀_def _ _ (fun _ _ _ ↦ map_intCast' _ (map_one _) _) _

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