piMap_image_pi_subset — Mathlib

English

Given a family of maps that are MapsTo on each coordinate, Pi.map preserves this relation on Pi-sets.

Русский

Дано семейство отображений, удовлетворяющих MapsTo на каждой координате, Pi.map сохраняет это отношение на Pi-множества.

LaTeX

$$$ \forall i, \mathrm{mem} I i \Rightarrow MapsTo (Pi.map f) (I.\pi s) (I.\pi t) $$$

Lean4

theorem piMap_image_pi_subset {f : ∀ i, α i → β i} (t : ∀ i, Set (α i)) :
    Pi.map f '' s.pi t ⊆ s.pi fun i ↦ f i '' t i :=
  image_subset_iff.2 <| piMap_mapsTo_pi fun _ _ => mapsTo_image _ _

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