natCast_def — Mathlib

English

For any i and natural n, the natural number n embeds into the direct limit as the class of (i,n): (n : DirectLimit G f) = ⟦⟨i,n⟩⟧, independent of i up to the identifications in the directed system.

Русский

Для любого индекса i и натурального числа n число n внедряется в прямой предел как класс пары (i,n): (n : DirectLimit G f) = ⟦⟨i,n⟩⟧, независимо от выбора i (с учётом эквивалентности в системе).

LaTeX

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

Lean4

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

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