nnratCast_def — Mathlib

English

For any index i and a nonnegative rational q, the natural embedding of q into the directed limit is represented by the pair (i,q).

Русский

Для каждого индекса i и неотрицательного рационального числа q естественное вложение q в направленный предел задаётся представлением в виде пары (i,q).

LaTeX

$$$\forall i:\, \mathbb{Q}_{\ge 0} \ni q: \; (q : \mathrm{DirectLimit}\ G f) = \llbracket i, q \rrbracket.$$$

Lean4

theorem nnratCast_def (q : ℚ≥0) (i) : (q : DirectLimit G f) = ⟦⟨i, q⟩⟧ :=
  map₀_def _ _ (fun _ _ _ ↦ map_nnratCast _ _) _

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