piMap_mapsTo_pi — Mathlib

English

A restatement of piMap_image_pi_subset using a general subset relation.

Русский

Переформулирование piMap_image_pi_subset через общую отношение подмножества.

LaTeX

$$$ \text{(same as 110543, restated)} $$$

Lean4

theorem piMap_mapsTo_pi {I : Set ι} {f : ∀ i, α i → β i} {s : ∀ i, Set (α i)} {t : ∀ i, Set (β i)}
    (h : ∀ i ∈ I, MapsTo (f i) (s i) (t i)) : MapsTo (Pi.map f) (I.pi s) (I.pi t) := fun _x hx i hi => h i hi (hx i hi)

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