Mathlib Map

Theorems · Theorem · order theory

Set.piMap_mapsTo_pi

∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {I : Set ι} {f : (i : ι) → α i → β i} {s : (i : ι) → Set (α i)}
  {t : (i : ι) → Set (β i)}, (∀ i ∈ I, Set.MapsTo (f i) (s i) (t i)) → Set.MapsTo (Pi.map f) (I.pi s) (I.pi t)
Defined in
Mathlib.Data.Set.Prod
Cited by
1 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Set.piMap_image_pi_subset · cited by 3Set.piMap_image_pi_subsetSet · cited by 53352SetSet.MapsTo · cited by 732Set.MapsToSet.pi · cited by 405Set.piPi.map · cited by 60Pi.mapSet.piMap_mapsTo_piCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Set.MapsTostatement and proof · cited by 732
  • Set.pistatement and proof · cited by 405
  • Pi.mapstatement · cited by 60

Cited by1

Results whose statement or proof uses this declaration.