prodMap — Mathlib

English

The prodMap construction composes two map-cluster-pt structures into a map-cluster-pt of the product, using the product filter la × lb.

Русский

Конструкция prodMap объединяет две структуры MapClusterPt в структуру для произведения, используя фильтр la × lb.

LaTeX

$$$$ \\text{MapClusterPt} x la f \\to \\text{MapClusterPt} (x,y) (la \\times lb) (Prod.map f g) $$$$

Lean4

theorem prodMap {α β : Type*} {f : α → X} {g : β → Y} {la : Filter α} {lb : Filter β} {x : X} {y : Y}
    (hf : MapClusterPt x la f) (hg : MapClusterPt y lb g) : MapClusterPt (x, y) (la ×ˢ lb) (.map f g) :=
  (hf.curry_prodMap hg).mono <| map_mono curry_le_prod

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