prodMap — Mathlib

English

If f,g have dense ranges, then Prod.map f g has dense range.

Русский

Если f и g имеют плотный образ, то отображение (f,g) имеет плотный образ.

LaTeX

$$$$\text{DenseRange}(f) \land \text{DenseRange}(g) \Rightarrow \text{DenseRange}(\mathrm{Prod.map}\,f\,g).$$$$

Lean4

/-- If `f` and `g` are maps with dense range, then `Prod.map f g` has dense range. -/
theorem prodMap {ι : Type*} {κ : Type*} {f : ι → Y} {g : κ → Z} (hf : DenseRange f) (hg : DenseRange g) :
    DenseRange (Prod.map f g) := by simpa only [DenseRange, prod_range_range_eq] using hf.prod hg

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