denseRange_coe₃ — Mathlib

English

DenseRange holds for the map x ↦ (coe' x.1, (coe' x.2, coe' x.3)) from α×β×γ to Completion α × Completion β × Completion γ.

Русский

Образ тройки координат плотности через отображение x ↦ (coe' x.1, (coe' x.2, coe' x.3)).

LaTeX

$$$\\mathrm{DenseRange}\\;\\big(\\;x\\mapsto (\\operatorname{coe}'x_{1}, (\\operatorname{coe}'x_{2}, \\operatorname{coe}'x_{3}))\\;\;\\big)$$$

Lean4

theorem denseRange_coe₃ :
    DenseRange fun x : α × β × γ => ((x.1 : Completion α), ((x.2.1 : Completion β), (x.2.2 : Completion γ))) :=
  denseRange_coe.prodMap denseRange_coe₂

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