piMap — Mathlib

English

If each f_i has dense range, then Pi.map f has dense range.

Русский

Если для каждого i образ f_i плотно насчитывается, то Pi.map f имеет плотный образ.

LaTeX

$$$$ \\text{DenseRange}(f_i) \\text{ for all } i \\Rightarrow \\text{DenseRange}(\\Pi.map f). $$$$

Lean4

theorem piMap {ι : Type*} {X Y : ι → Type*} [∀ i, TopologicalSpace (Y i)] {f : (i : ι) → (X i) → (Y i)}
    (hf : ∀ i, DenseRange (f i)) : DenseRange (Pi.map f) :=
  by
  rw [DenseRange, Set.range_piMap]
  exact dense_pi Set.univ (fun i _ => hf i)

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