denseRange_coe₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem denseRange_coe₂ : DenseRange fun x : α × β => ((x.1 : Completion α), (x.2 : Completion β)) :=
  denseRange_coe.prodMap denseRange_coe

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