Loogle!

Result

Found 323 declarations mentioning Prod.map. Of these, only the first 200 are shown.

• Prod.map 📋 Init.Core
  {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
• Prod.map_fst 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (Prod.map f g x).1 = f x.1
• Prod.map_snd 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (Prod.map f g x).2 = g x.2
• Prod.map_apply 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α) (y : γ) : Prod.map f g (x, y) = (f x, g y)
• Prod.map_id 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} : Prod.map id id = id
• Prod.map_id' 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} : (Prod.map (fun a => a) fun b => b) = fun x => x
• Prod.map_map 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) (x : α × γ) : Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x
• Prod.map_comp_swap 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) : Prod.map f g ∘ Prod.swap = Prod.swap ∘ Prod.map g f
• Prod.map_comp_map 📋 Init.Data.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ) (g : β → ε) (g' : δ → ζ) : Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')
• List.zip_map_left 📋 Init.Data.List.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {l₁ : List α} {l₂ : List β} : (List.map f l₁).zip l₂ = List.map (Prod.map f id) (l₁.zip l₂)
• List.zip_map_right 📋 Init.Data.List.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {l₁ : List α} {l₂ : List β} : l₁.zip (List.map f l₂) = List.map (Prod.map id f) (l₁.zip l₂)
• List.zip_map 📋 Init.Data.List.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {l₁ : List α} {l₂ : List β} : (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
• List.map_snd_add_zipIdx_eq_zipIdx 📋 Init.Data.List.Range
  {α : Type u_1} {l : List α} {n k : ℕ} : List.map (Prod.map id fun x => x + n) (l.zipIdx k) = l.zipIdx (n + k)
• List.zipIdx_cons' 📋 Init.Data.List.Range
  {α : Type u_1} {i : ℕ} {x : α} {xs : List α} : (x :: xs).zipIdx i = (x, i) :: List.map (Prod.map id fun x => x + 1) (xs.zipIdx i)
• List.unzip_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {as : List (α × β)} : as.toArray.unzip = Prod.map List.toArray List.toArray as.unzip
• List.map_zipIdx 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {k : ℕ} : List.map (Prod.map f id) (l.zipIdx k) = (List.map f l).zipIdx k
• List.zipIdx_map 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} {l : List α} {k : ℕ} {f : α → β} : (List.map f l).zipIdx k = List.map (Prod.map f id) (l.zipIdx k)
• Array.zip_map_left 📋 Init.Data.Array.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : α → γ} {as : Array α} {bs : Array β} : (Array.map f as).zip bs = Array.map (Prod.map f id) (as.zip bs)
• Array.zip_map_right 📋 Init.Data.Array.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {f : β → γ} {as : Array α} {bs : Array β} : as.zip (Array.map f bs) = Array.map (Prod.map id f) (as.zip bs)
• Array.zip_map 📋 Init.Data.Array.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {as : Array α} {bs : Array β} : (Array.map f as).zip (Array.map g bs) = Array.map (Prod.map f g) (as.zip bs)
• Array.map_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {k : ℕ} : Array.map (Prod.map f id) (xs.zipIdx k) = (Array.map f xs).zipIdx k
• Array.zipIdx_map 📋 Init.Data.Array.Range
  {α : Type u_1} {β : Type u_2} {xs : Array α} {k : ℕ} {f : α → β} : (Array.map f xs).zipIdx k = Array.map (Prod.map f id) (xs.zipIdx k)
• Array.map_snd_add_zipIdx_eq_zipIdx 📋 Init.Data.Array.Range
  {α : Type u_1} {xs : Array α} {n k : ℕ} : Array.map (Prod.map id fun x => x + n) (xs.zipIdx k) = xs.zipIdx (n + k)
• Vector.zip_map_left 📋 Init.Data.Vector.Zip
  {α : Type u_1} {γ : Type u_2} {n : ℕ} {β : Type u_3} {f : α → γ} {as : Vector α n} {bs : Vector β n} : (Vector.map f as).zip bs = Vector.map (Prod.map f id) (as.zip bs)
• Vector.zip_map_right 📋 Init.Data.Vector.Zip
  {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {f : β → γ} {as : Vector α n} {bs : Vector β n} : as.zip (Vector.map f bs) = Vector.map (Prod.map id f) (as.zip bs)
• Vector.zip_map 📋 Init.Data.Vector.Zip
  {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {n : ℕ} {f : α → γ} {g : β → δ} {as : Vector α n} {bs : Vector β n} : (Vector.map f as).zip (Vector.map g bs) = Vector.map (Prod.map f g) (as.zip bs)
• Vector.map_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ} : Vector.map (Prod.map f id) (xs.zipIdx k) = (Vector.map f xs).zipIdx k
• Vector.zipIdx_map 📋 Init.Data.Vector.Range
  {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {k : ℕ} : (Vector.map f xs).zipIdx k = Vector.map (Prod.map f id) (xs.zipIdx k)
• Vector.map_snd_add_zipIdx_eq_zipIdx 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} {xs : Vector α n} {m k : ℕ} : Vector.map (Prod.map id fun x => x + m) (xs.zipIdx k) = xs.zipIdx (m + k)
• Function.uncurry_bicompl 📋 Mathlib.Logic.Function.Defs
  {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} {ε : Sort u_10} (f : γ → δ → ε) (g : α → γ) (h : β → δ) : Function.uncurry (Function.bicompl f g h) = Function.uncurry f ∘ Prod.map g h
• Function.Involutive.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} : Function.Involutive f → Function.Involutive g → Function.Involutive (Prod.map f g)
• Prod.map_involutive 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] {f : α → α} {g : β → β} : Function.Involutive (Prod.map f g) ↔ Function.Involutive f ∧ Function.Involutive g
• Function.Bijective.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Function.Bijective f) (hg : Function.Bijective g) : Function.Bijective (Prod.map f g)
• Function.Injective.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Function.Injective f) (hg : Function.Injective g) : Function.Injective (Prod.map f g)
• Function.Semiconj.swap_map 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) : Function.Semiconj Prod.swap (Prod.map f g) (Prod.map g f)
• Function.Surjective.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} (hf : Function.Surjective f) (hg : Function.Surjective g) : Function.Surjective (Prod.map f g)
• Prod.map_apply' 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) (p : α × β) : Prod.map f g p = (f p.1, g p.2)
• Prod.map_bijective 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} : Function.Bijective (Prod.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
• Prod.map_injective 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} : Function.Injective (Prod.map f g) ↔ Function.Injective f ∧ Function.Injective g
• Prod.map_surjective 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} : Function.Surjective (Prod.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
• Prod.map_def 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} : Prod.map f g = fun p => (f p.1, g p.2)
• Prod.map_iterate 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : ℕ) : (Prod.map f g)^[n] = Prod.map f^[n] g^[n]
• Prod.map_fst' 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) : Prod.fst ∘ Prod.map f g = f ∘ Prod.fst
• Prod.map_snd' 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) : Prod.snd ∘ Prod.map f g = g ∘ Prod.snd
• Function.LeftInverse.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} (hf : Function.LeftInverse f₁ f₂) (hg : Function.LeftInverse g₁ g₂) : Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
• Function.RightInverse.prodMap 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} : Function.RightInverse f₁ f₂ → Function.RightInverse g₁ g₂ → Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
• Prod.map_leftInverse 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} : Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.LeftInverse f₁ f₂ ∧ Function.LeftInverse g₁ g₂
• Prod.map_rightInverse 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ} : Function.RightInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.RightInverse f₁ f₂ ∧ Function.RightInverse g₁ g₂
• Antitone.prodMap 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : Antitone f) (hg : Antitone g) : Antitone (Prod.map f g)
• Monotone.prodMap 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : Monotone f) (hg : Monotone g) : Monotone (Prod.map f g)
• StrictAnti.prodMap 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [PartialOrder α] [PartialOrder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : StrictAnti f) (hg : StrictAnti g) : StrictAnti (Prod.map f g)
• StrictMono.prodMap 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} [PartialOrder α] [PartialOrder β] [Preorder γ] [Preorder δ] {f : α → γ} {g : β → δ} (hf : StrictMono f) (hg : StrictMono g) : StrictMono (Prod.map f g)
• Prod.instCanLift 📋 Mathlib.Tactic.Lift
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {coeβα : β → α} {condβα : α → Prop} {coeδγ : δ → γ} {condδγ : γ → Prop} [CanLift α β coeβα condβα] [CanLift γ δ coeδγ condδγ] : CanLift (α × γ) (β × δ) (Prod.map coeβα coeδγ) fun x => condβα x.1 ∧ condδγ x.2
• optionProdEquiv_symm_inr 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_9} {β : Type u_10} (p : α × β) : optionProdEquiv.symm (Sum.inr p) = Prod.map some id p
• Equiv.prodCongr_apply 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {α₂ : Type u_10} {β₁ : Type u_11} {β₂ : Type u_12} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : ⇑(e₁.prodCongr e₂) = Prod.map ⇑e₁ ⇑e₂
• Set.range_prodMap 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} : Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
• Set.EqOn.left_of_eqOn_prodMap 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ} (h : Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)) (ht : t.Nonempty) : Set.EqOn f f' s
• Set.EqOn.right_of_eqOn_prodMap 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ} (h : Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)) (hs : s.Nonempty) : Set.EqOn g g' t
• Set.EqOn.prodMap 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f f' : α → γ} {g g' : β → δ} (hf : Set.EqOn f f' s) (hg : Set.EqOn g g' t) : Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t)
• Set.preimage_prod_map_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ) : Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
• Set.prodMap_image_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (s : Set α) (t : Set γ) : Prod.map f g '' s ×ˢ t = (f '' s) ×ˢ (g '' t)
• Set.preimage_coe_coe_diagonal 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} (s : Set α) : (Prod.map (fun x => ↑x) fun x => ↑x) ⁻¹' Set.diagonal α = Set.diagonal ↑s
• Set.eqOn_prodMap_iff 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f f' : α → γ} {g g' : β → δ} {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : Set.EqOn (Prod.map f g) (Prod.map f' g') (s ×ˢ t) ↔ Set.EqOn f f' s ∧ Set.EqOn g g' t
• Set.graphOn_prod_graphOn 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : Set.graphOn f s ×ˢ Set.graphOn g t = ⇑(Equiv.prodProdProdComm α γ β δ) ⁻¹' Set.graphOn (Prod.map f g) (s ×ˢ t)
• Set.graphOn_prod_prodMap 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ) : Set.graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' Set.graphOn f s ×ˢ Set.graphOn g t
• Set.mapsTo_prodMap_diagonal 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {f : α → β} : Set.MapsTo (Prod.map f f) (Set.diagonal α) (Set.diagonal β)
• AddHom.coe_prodMap 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• MulHom.coe_prodMap 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• AddMonoidHom.coe_prodMap 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• MonoidHom.coe_prodMap 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• Function.Embedding.coe_prodMap 📋 Mathlib.Logic.Embedding.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : ⇑(e₁.prodMap e₂) = Prod.map ⇑e₁ ⇑e₂
• RelEmbedding.prodLexMap_apply 📋 Mathlib.Order.RelIso.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} {u : δ → δ → Prop} (f : r ↪r s) (g : t ↪r u) (a✝ : α × γ) : (f.prodLexMap g) a✝ = Prod.map (⇑f) (⇑g) a✝
• OrderHom.prodMap_coe 📋 Mathlib.Order.Hom.Basic
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (f : α →o β) (g : γ →o δ) (a✝ : α × γ) : (f.prodMap g) a✝ = Prod.map (⇑f) (⇑g) a✝
• List.map_prodMap_offDiag 📋 Mathlib.Data.List.OffDiag
  {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map (Prod.map f f) l.offDiag = (List.map f l).offDiag
• Finset.prodMap_image_product 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq β] [DecidableEq δ] (f : α → β) (g : γ → δ) (s : Finset α) (t : Finset γ) : Finset.image (Prod.map f g) (s ×ˢ t) = Finset.image f s ×ˢ Finset.image g t
• RingEquiv.coe_prodCongr 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') : ⇑(f.prodCongr g) = Prod.map ⇑f ⇑g
• RingEquiv.prodCongr_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') (a✝ : R × S) : (f.prodCongr g) a✝ = Prod.map (⇑f) (⇑g) a✝
• RingEquiv.prodCongr_symm_apply 📋 Mathlib.Algebra.Ring.Equiv
  {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') (a✝ : R' × S') : (f.prodCongr g).symm a✝ = Prod.map (⇑f.symm) (⇑g.symm) a✝
• Prod.Lex.prodLexCongr_apply 📋 Mathlib.Order.Hom.Lex
  {α : Type u_4} {β : Type u_5} {γ : Type u_6} {δ : Type u_7} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ] (ea : α ≃o β) (eb : γ ≃o δ) (a✝ : Lex (α × γ)) : (Prod.Lex.prodLexCongr ea eb) a✝ = toLex (Prod.map (⇑ea) (⇑eb) (ofLex a✝))
• Prod.Lex.sumLexProdLexDistrib_apply 📋 Mathlib.Order.Hom.Lex
  (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex ((α ⊕ₗ β) × γ)) : (Prod.Lex.sumLexProdLexDistrib α β γ) a✝ = toLex (Sum.map (⇑toLex) (⇑toLex) ((Equiv.sumProdDistrib α β γ) (Prod.map (⇑ofLex) id (ofLex a✝))))
• Prod.Lex.sumLexProdLexDistrib_symm_apply 📋 Mathlib.Order.Hom.Lex
  (α : Type u_4) (β : Type u_5) (γ : Type u_6) [Preorder α] [Preorder β] [Preorder γ] (a✝ : Lex (α × γ) ⊕ₗ Lex (β × γ)) : (RelIso.symm (Prod.Lex.sumLexProdLexDistrib α β γ)) a✝ = toLex (Prod.map (⇑toLex) id ((Equiv.sumProdDistrib α β γ).symm (Sum.map (⇑ofLex) (⇑ofLex) (ofLex a✝))))
• AddActionHom.prodMap_apply 📋 Mathlib.GroupTheory.GroupAction.Hom
  {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [VAdd M α] [VAdd M β] [VAdd N γ] [VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• MulActionHom.prodMap_apply 📋 Mathlib.GroupTheory.GroupAction.Hom
  {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} [SMul M α] [SMul M β] [SMul N γ] [SMul N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : β →ₑ[σ] δ) : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• NonUnitalRingHom.coe_prodMap 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• RingHom.coe_prodMap 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• AlgEquiv.linearEquivConj_mulLeftRight 📋 Mathlib.Algebra.Algebra.Equiv
  {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂] (f : A₁ ≃ₐ[R] A₂) (x : A₁ × A₁) : (↑f).conj (LinearMap.mulLeftRight R x) = LinearMap.mulLeftRight R (Prod.map (⇑f) (⇑f) x)
• Finset.prodMk_inf'_inf' 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.inf' hs f, t.inf' ht g) = (s ×ˢ t).inf' ⋯ (Prod.map f g)
• Finset.prodMk_sup'_sup' 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s.sup' hs f, t.sup' ht g) = (s ×ˢ t).sup' ⋯ (Prod.map f g)
• Finset.inf'_prodMap 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf' hst (Prod.map f g) = (s.inf' ⋯ f, t.inf' ⋯ g)
• Finset.sup'_prodMap 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] {s : Finset ι} {t : Finset κ} (hst : (s ×ˢ t).Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup' hst (Prod.map f g) = (s.sup' ⋯ f, t.sup' ⋯ g)
• Finset.inf_prodMap 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeInf α] [SemilatticeInf β] [OrderTop α] [OrderTop β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).inf (Prod.map f g) = (s.inf f, t.inf g)
• Finset.sup_prodMap 📋 Mathlib.Data.Finset.Lattice.Prod
  {ι : Type u_7} {κ : Type u_8} {α : Type u_9} {β : Type u_10} [SemilatticeSup α] [SemilatticeSup β] [OrderBot α] [OrderBot β] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) : (s ×ˢ t).sup (Prod.map f g) = (s.sup f, t.sup g)
• Multiset.antidiagonal_cons 📋 Mathlib.Data.Multiset.Antidiagonal
  {α : Type u_1} (a : α) (s : Multiset α) : (a ::ₘ s).antidiagonal = Multiset.map (Prod.map id (Multiset.cons a)) s.antidiagonal + Multiset.map (Prod.map (Multiset.cons a) id) s.antidiagonal
• LinearMap.coe_prodMap 📋 Mathlib.LinearAlgebra.Prod
  {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄] [Module R M] [Module R M₂] [Module R M₃] [Module R M₄] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• List.Nat.antidiagonal_succ 📋 Mathlib.Data.List.NatAntidiagonal
  {n : ℕ} : List.Nat.antidiagonal (n + 1) = (0, n + 1) :: List.map (Prod.map Nat.succ id) (List.Nat.antidiagonal n)
• List.Nat.antidiagonal_succ' 📋 Mathlib.Data.List.NatAntidiagonal
  {n : ℕ} : List.Nat.antidiagonal (n + 1) = List.map (Prod.map id Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 1, 0)]
• List.Nat.antidiagonal_succ_succ' 📋 Mathlib.Data.List.NatAntidiagonal
  {n : ℕ} : List.Nat.antidiagonal (n + 2) = (0, n + 2) :: List.map (Prod.map Nat.succ Nat.succ) (List.Nat.antidiagonal n) ++ [(n + 2, 0)]
• Multiset.Nat.antidiagonal_succ 📋 Mathlib.Data.Multiset.NatAntidiagonal
  {n : ℕ} : Multiset.Nat.antidiagonal (n + 1) = (0, n + 1) ::ₘ Multiset.map (Prod.map Nat.succ id) (Multiset.Nat.antidiagonal n)
• Multiset.Nat.antidiagonal_succ' 📋 Mathlib.Data.Multiset.NatAntidiagonal
  {n : ℕ} : Multiset.Nat.antidiagonal (n + 1) = (n + 1, 0) ::ₘ Multiset.map (Prod.map id Nat.succ) (Multiset.Nat.antidiagonal n)
• Multiset.Nat.antidiagonal_succ_succ' 📋 Mathlib.Data.Multiset.NatAntidiagonal
  {n : ℕ} : Multiset.Nat.antidiagonal (n + 2) = (0, n + 2) ::ₘ (n + 2, 0) ::ₘ Multiset.map (Prod.map Nat.succ Nat.succ) (Multiset.Nat.antidiagonal n)
• Finsupp.image_prodMap_embDomain_antidiagonal 📋 Mathlib.Data.Finsupp.Antidiagonal
  {α : Type u} [DecidableEq α] {β : Type u_1} [DecidableEq β] (f : α ↪ β) (y : α →₀ ℕ) : Finset.image (Prod.map (Finsupp.embDomain f) (Finsupp.embDomain f)) (Finset.antidiagonal y) = Finset.antidiagonal (Finsupp.embDomain f y)
• Function.IsFixedPt.prodMap 📋 Mathlib.Dynamics.PeriodicPts.Defs
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β} (ha : Function.IsFixedPt f a) (hb : Function.IsFixedPt g b) : Function.IsFixedPt (Prod.map f g) (a, b)
• Function.IsPeriodicPt.prodMap 📋 Mathlib.Dynamics.PeriodicPts.Defs
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {a : α} {b : β} {n : ℕ} (ha : Function.IsPeriodicPt f n a) (hb : Function.IsPeriodicPt g n b) : Function.IsPeriodicPt (Prod.map f g) n (a, b)
• Function.isFixedPt_prodMap 📋 Mathlib.Dynamics.PeriodicPts.Defs
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} (x : α × β) : Function.IsFixedPt (Prod.map f g) x ↔ Function.IsFixedPt f x.1 ∧ Function.IsFixedPt g x.2
• Function.isPeriodicPt_prodMap 📋 Mathlib.Dynamics.PeriodicPts.Defs
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {n : ℕ} (x : α × β) : Function.IsPeriodicPt (Prod.map f g) n x ↔ Function.IsPeriodicPt f n x.1 ∧ Function.IsPeriodicPt g n x.2
• Function.minimalPeriod_fst_dvd 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : Function.minimalPeriod f x.1 ∣ Function.minimalPeriod (Prod.map f g) x
• Function.minimalPeriod_snd_dvd 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : Function.minimalPeriod g x.2 ∣ Function.minimalPeriod (Prod.map f g) x
• Function.minimalPeriod_prodMap 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β) : Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (Function.minimalPeriod g x.2)
• Filter.Tendsto.prodMap_coprod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Filter.Tendsto f a c) (hg : Filter.Tendsto g b d) : Filter.Tendsto (Prod.map f g) (a.coprod b) (c.coprod d)
• Filter.prod_map_left 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (F : Filter α) (G : Filter γ) : Filter.map f F ×ˢ G = Filter.map (Prod.map f id) (F ×ˢ G)
• Filter.prod_map_right 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β → γ) (F : Filter α) (G : Filter β) : F ×ˢ Filter.map f G = Filter.map (Prod.map id f) (F ×ˢ G)
• Filter.map_prodMap_coprod_le 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : α₁ → β₁} {m₂ : α₂ → β₂} : Filter.map (Prod.map m₁ m₂) (f₁.coprod f₂) ≤ (Filter.map m₁ f₁).coprod (Filter.map m₂ f₂)
• Filter.EventuallyEq.prodMap 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {la : Filter α} {fa ga : α → γ} (ha : fa =ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ} (hb : fb =ᶠ[lb] gb) : Prod.map fa fb =ᶠ[la ×ˢ lb] Prod.map ga gb
• Filter.comap_prodMap_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ) : Filter.comap (Prod.map f g) (lb ×ˢ ld) = Filter.comap f lb ×ˢ Filter.comap g ld
• Filter.prod_map_map_eq' 📋 Mathlib.Order.Filter.Prod
  {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} (f : α₁ → α₂) (g : β₁ → β₂) (F : Filter α₁) (G : Filter β₁) : Filter.map f F ×ˢ Filter.map g G = Filter.map (Prod.map f g) (F ×ˢ G)
• Filter.Tendsto.prodMap 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} {f : α → γ} {g : β → δ} {a : Filter α} {b : Filter β} {c : Filter γ} {d : Filter δ} (hf : Filter.Tendsto f a c) (hg : Filter.Tendsto g b d) : Filter.Tendsto (Prod.map f g) (a ×ˢ b) (c ×ˢ d)
• Filter.map_prodMap_const_id_principal_coprod_principal 📋 Mathlib.Order.Filter.Prod
  {α : Type u_6} {β : Type u_7} {ι : Type u_8} (a : α) (b : β) (i : ι) : Filter.map (Prod.map (fun x => b) id) ((Filter.principal {a}).coprod (Filter.principal {i})) = Filter.principal ({b} ×ˢ Set.univ)
• Filter.EventuallyLE.prodMap 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} [LE γ] [LE δ] {la : Filter α} {fa ga : α → γ} (ha : fa ≤ᶠ[la] ga) {lb : Filter β} {fb gb : β → δ} (hb : fb ≤ᶠ[lb] gb) : Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb
• DenseRange.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {Y : Type v} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {ι : Type u_5} {κ : Type u_6} {f : ι → Y} {g : κ → Z} (hf : DenseRange f) (hg : DenseRange g) : DenseRange (Prod.map f g)
• Continuous.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : Z → X} {g : W → Y} (hf : Continuous f) (hg : Continuous g) : Continuous (Prod.map f g)
• IsOpenMap.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Prod.map f g)
• IsOpenQuotientMap.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) : IsOpenQuotientMap (Prod.map f g)
• Topology.IsClosedEmbedding.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsClosedEmbedding f) (hg : Topology.IsClosedEmbedding g) : Topology.IsClosedEmbedding (Prod.map f g)
• Topology.IsEmbedding.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsEmbedding f) (hg : Topology.IsEmbedding g) : Topology.IsEmbedding (Prod.map f g)
• Topology.IsInducing.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsInducing f) (hg : Topology.IsInducing g) : Topology.IsInducing (Prod.map f g)
• Topology.IsOpenEmbedding.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : Topology.IsOpenEmbedding f) (hg : Topology.IsOpenEmbedding g) : Topology.IsOpenEmbedding (Prod.map f g)
• ContinuousAt.prodMap' 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {x : X} {y : Y} (hf : ContinuousAt f x) (hg : ContinuousAt g y) : ContinuousAt (Prod.map f g) (x, y)
• ContinuousAt.prodMap 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Z} {g : Y → W} {p : X × Y} (hf : ContinuousAt f p.1) (hg : ContinuousAt g p.2) : ContinuousAt (Prod.map f g) p
• Filter.EventuallyEq.prodMap_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ =ᶠ[nhds x] f₂) (hg : g₁ =ᶠ[nhds y] g₂) : Prod.map f₁ g₁ =ᶠ[nhds (x, y)] Prod.map f₂ g₂
• Filter.EventuallyLE.prodMap_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} [LE α] [LE β] {f₁ f₂ : X → α} {g₁ g₂ : Y → β} {x : X} {y : Y} (hf : f₁ ≤ᶠ[nhds x] f₂) (hg : g₁ ≤ᶠ[nhds y] g₂) : Prod.map f₁ g₁ ≤ᶠ[nhds (x, y)] Prod.map f₂ g₂
• Filter.Tendsto.prodMap_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W} (hf : Filter.Tendsto f (nhds x) (nhds y)) (hg : Filter.Tendsto g (nhds z) (nhds w)) : Filter.Tendsto (Prod.map f g) (nhds (x, z)) (nhds (y, w))
• Homeomorph.coe_prodCongr 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6} [TopologicalSpace X'] [TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') : ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
• SetRel.isRefl_preimage 📋 Mathlib.Data.Rel
  {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsRefl] : SetRel.IsRefl (Prod.map f f ⁻¹' R)
• SetRel.isSymm_image 📋 Mathlib.Data.Rel
  {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : α → β} [R.IsSymm] : SetRel.IsSymm (Prod.map f f '' R)
• SetRel.isSymm_preimage 📋 Mathlib.Data.Rel
  {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsSymm] : SetRel.IsSymm (Prod.map f f ⁻¹' R)
• SetRel.isTrans_preimage 📋 Mathlib.Data.Rel
  {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsTrans] : SetRel.IsTrans (Prod.map f f ⁻¹' R)
• MapClusterPt.curry_prodMap 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {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.curry lb) (Prod.map f g)
• MapClusterPt.prodMap 📋 Mathlib.Topology.Constructions
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {α : Type u_5} {β : Type u_6} {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) (Prod.map f g)
• ContinuousOn.prodMap 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} (hf : ContinuousOn f s) (hg : ContinuousOn g t) : ContinuousOn (Prod.map f g) (s ×ˢ t)
• ContinuousWithinAt.prodMap 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {f : α → γ} {g : β → δ} {s : Set α} {t : Set β} {x : α} {y : β} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g t y) : ContinuousWithinAt (Prod.map f g) (s ×ˢ t) (x, y)
• uniformity_comap 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} {x✝ : UniformSpace β} (f : α → β) : uniformity α = Filter.comap (Prod.map f f) (uniformity β)
• ball_preimage 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} {f : α → β} {U : SetRel β β} {x : α} : UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U
• UniformContinuous.prodMap 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] {f : α → γ} {g : β → δ} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous (Prod.map f g)
• uniformity_additive 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity (Additive α) = Filter.map (Prod.map ⇑Additive.ofMul ⇑Additive.ofMul) (uniformity α)
• uniformity_multiplicative 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} [UniformSpace α] : uniformity (Multiplicative α) = Filter.map (Prod.map ⇑Multiplicative.ofAdd ⇑Multiplicative.ofAdd) (uniformity α)
• map_uniformity_set_coe 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {s : Set α} [UniformSpace α] : Filter.map (Prod.map Subtype.val Subtype.val) (uniformity ↑s) = uniformity α ⊓ Filter.principal (s ×ˢ s)
• Sum.uniformity 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : uniformity (α ⊕ β) = Filter.map (Prod.map Sum.inl Sum.inl) (uniformity α) ⊔ Filter.map (Prod.map Sum.inr Sum.inr) (uniformity β)
• uniformity_setCoe 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {s : Set α} [UniformSpace α] : uniformity ↑s = Filter.comap (Prod.map Subtype.val Subtype.val) (uniformity α)
• union_mem_uniformity_sum 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] {a : SetRel α α} (ha : a ∈ uniformity α) {b : SetRel β β} (hb : b ∈ uniformity β) : Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)
• Filter.Tendsto.prod_atBot 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {γ : Type u_5} [Preorder α] [Preorder γ] {f g : α → γ} (hf : Filter.Tendsto f Filter.atBot Filter.atBot) (hg : Filter.Tendsto g Filter.atBot Filter.atBot) : Filter.Tendsto (Prod.map f g) Filter.atBot Filter.atBot
• Filter.Tendsto.prod_atTop 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {γ : Type u_5} [Preorder α] [Preorder γ] {f g : α → γ} (hf : Filter.Tendsto f Filter.atTop Filter.atTop) (hg : Filter.Tendsto g Filter.atTop Filter.atTop) : Filter.Tendsto (Prod.map f g) Filter.atTop Filter.atTop
• Filter.prod_map_atBot_eq 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : Filter.map u₁ Filter.atBot ×ˢ Filter.map u₂ Filter.atBot = Filter.map (Prod.map u₁ u₂) Filter.atBot
• Filter.prod_map_atTop_eq 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α₁ : Type u_6} {α₂ : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} [Preorder β₁] [Preorder β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) : Filter.map u₁ Filter.atTop ×ˢ Filter.map u₂ Filter.atTop = Filter.map (Prod.map u₁ u₂) Filter.atTop
• Filter.Tendsto.prod_map_prod_atBot 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Filter.Tendsto f F Filter.atBot) (hg : Filter.Tendsto g G Filter.atBot) : Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot
• Filter.Tendsto.prod_map_prod_atTop 📋 Mathlib.Order.Filter.AtTopBot.Prod
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder γ] {F : Filter α} {G : Filter β} {f : α → γ} {g : β → γ} (hf : Filter.Tendsto f F Filter.atTop) (hg : Filter.Tendsto g G Filter.atTop) : Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atTop
• SeparationQuotient.isQuotientMap_prodMap_mk 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] : Topology.IsQuotientMap (Prod.map SeparationQuotient.mk SeparationQuotient.mk)
• SeparationQuotient.map_prod_map_mk_nhds 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) : Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (nhds (x, y)) = nhds (SeparationQuotient.mk x, SeparationQuotient.mk y)
• SeparationQuotient.continuousOn_lift₂ 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {s : Set (SeparationQuotient X × SeparationQuotient Y)} : ContinuousOn (Function.uncurry (SeparationQuotient.lift₂ f hf)) s ↔ ContinuousOn (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)
• SeparationQuotient.continuousWithinAt_lift₂ 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y → Z} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y} : ContinuousWithinAt (Function.uncurry (SeparationQuotient.lift₂ f hf)) s (SeparationQuotient.mk x, SeparationQuotient.mk y) ↔ ContinuousWithinAt (Function.uncurry f) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s) (x, y)
• SeparationQuotient.tendsto_lift₂_nhdsWithin 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → α} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {x : X} {y : Y} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} : Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (nhdsWithin (SeparationQuotient.mk x, SeparationQuotient.mk y) s) l ↔ Filter.Tendsto (Function.uncurry f) (nhdsWithin (x, y) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)) l
• IsDenseInducing.prodMap 📋 Mathlib.Topology.DenseEmbedding
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ} (de₁ : IsDenseInducing e₁) (de₂ : IsDenseInducing e₂) : IsDenseInducing (Prod.map e₁ e₂)
• IsHomeomorph.prodMap 📋 Mathlib.Topology.Homeomorph.Lemmas
  {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {W : Type u_5} [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsHomeomorph f) (hg : IsHomeomorph g) : IsHomeomorph (Prod.map f g)
• ContinuousMap.prodMap_apply 📋 Mathlib.Topology.ContinuousMap.Basic
  {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [TopologicalSpace α₁] [TopologicalSpace α₂] [TopologicalSpace β₁] [TopologicalSpace β₂] (f : C(α₁, α₂)) (g : C(β₁, β₂)) (a✝ : α₁ × β₁) : (f.prodMap g) a✝ = Prod.map (⇑f) (⇑g) a✝
• IsProperMap.universally_closed 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (Z : Type u_6) [TopologicalSpace Z] (h : IsProperMap f) : IsClosedMap (Prod.map f id)
• IsProperMap.prodMap 📋 Mathlib.Topology.Maps.Proper.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {W : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] {f : X → Y} {g : Z → W} (hf : IsProperMap f) (hg : IsProperMap g) : IsProperMap (Prod.map f g)
• CauchySeq.tendsto_uniformity 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Preorder β] {u : β → α} (h : CauchySeq u) : Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
• CauchySeq.prodMap 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} {δ : Type u_2} [UniformSpace β] [Preorder γ] [Preorder δ] {u : γ → α} {v : δ → β} (hu : CauchySeq u) (hv : CauchySeq v) : CauchySeq (Prod.map u v)
• cauchySeq_iff_tendsto 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
• cauchySeq_iff' 📋 Mathlib.Topology.UniformSpace.Cauchy
  {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α} : CauchySeq u ↔ ∀ V ∈ uniformity α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V
• SeparationQuotient.comap_mk_uniformity 📋 Mathlib.Topology.UniformSpace.Separation
  {α : Type u} [UniformSpace α] : Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity (SeparationQuotient α)) = uniformity α
• SeparationQuotient.uniformity_eq 📋 Mathlib.Topology.UniformSpace.Separation
  {α : Type u} [UniformSpace α] : uniformity (SeparationQuotient α) = Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)
• SeparationQuotient.comap_map_mk_uniformity 📋 Mathlib.Topology.UniformSpace.Separation
  {α : Type u} [UniformSpace α] : Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity α)) = uniformity α
• IsUniformInducing.basis_uniformity 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} (hf : IsUniformInducing f) {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (β × β)} (H : (uniformity β).HasBasis p s) : (uniformity α).HasBasis p fun i => Prod.map f f ⁻¹' s i
• isUniformInducing_iff' 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} : IsUniformInducing f ↔ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
• isUniformEmbedding_iff' 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {α : Type u} {β : Type v} [UniformSpace α] [UniformSpace β] {f : α → β} : IsUniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
• comap_uniformity_of_spaced_out 📋 Mathlib.Topology.UniformSpace.UniformEmbedding
  {β : Type v} [UniformSpace β] {α : Type u_1} {f : α → β} {s : Set (β × β)} (hs : s ∈ uniformity β) (hf : Pairwise fun x y => (f x, f y) ∉ s) : Filter.comap (Prod.map f f) (uniformity β) = Filter.principal SetRel.id
• ContinuousLinearMap.coe_prodMap' 📋 Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
  {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : ⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
• UniformEquiv.coe_prodCongr 📋 Mathlib.Topology.UniformSpace.Equiv
  {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} [UniformSpace α] [UniformSpace β] [UniformSpace γ] [UniformSpace δ] (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : ⇑(h₁.prodCongr h₂) = Prod.map ⇑h₁ ⇑h₂
• TendstoUniformly.prodMap 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')
• UniformCauchySeqOn.prodMap 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'} {s' : Set α'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s') : UniformCauchySeqOn (fun i => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')
• TendstoUniformlyOn.prodMap 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} {s' : Set α'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s') : TendstoUniformlyOn (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')
• TendstoUniformlyOnFilter.prodMap 📋 Mathlib.Topology.UniformSpace.UniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_5} {α' : Type u_6} {β' : Type u_7} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : Filter ι'} {q' : Filter α'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q q') : TendstoUniformlyOnFilter (fun i => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')
• UniformOnFun.gen_eq_preimage_restrict 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (S : Set α) (V : Set (β × β)) : UniformOnFun.gen 𝔖 S V = Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
• IsDenseInducing.extend_Z_bilin 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {G : Type u_5} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [TopologicalSpace β] [AddCommGroup β] [TopologicalSpace γ] [AddCommGroup γ] [IsTopologicalAddGroup γ] [TopologicalSpace δ] [AddCommGroup δ] [UniformSpace G] [AddCommGroup G] {e : β →+ α} (de : IsDenseInducing ⇑e) {f : δ →+ γ} (df : IsDenseInducing ⇑f) {φ : β →+ δ →+ G} (hφ : Continuous fun p => (φ p.1) p.2) [IsUniformAddGroup G] [T0Space G] [CompleteSpace G] : Continuous (⋯.extend fun p => (φ p.1) p.2)
• Matrix.kroneckerMap_submatrix_left 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {l' : Type u_15} {m' : Type u_16} (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (r : l' → l) (c : m' → m) : Matrix.kroneckerMap f (A.submatrix r c) B = (Matrix.kroneckerMap f A B).submatrix (Prod.map r id) (Prod.map c id)
• Matrix.kroneckerMap_submatrix_right 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {n' : Type u_17} {p' : Type u_18} (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (r : n' → n) (c : p' → p) : Matrix.kroneckerMap f A (B.submatrix r c) = (Matrix.kroneckerMap f A B).submatrix (Prod.map id r) (Prod.map id c)
• Matrix.kroneckerMap_submatrix_submatrix 📋 Mathlib.LinearAlgebra.Matrix.Kronecker
  {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17} {p' : Type u_18} (f : α → β → γ) (A : Matrix l m α) (B : Matrix n p β) (r : l' → l) (c : m' → m) (r' : n' → n) (c' : p' → p) : Matrix.kroneckerMap f (A.submatrix r c) (B.submatrix r' c') = (Matrix.kroneckerMap f A B).submatrix (Prod.map r r') (Prod.map c c')
• Stream'.Seq.zip_map_left 📋 Mathlib.Data.Seq.Basic
  {α : Type u} {β : Type v} {α' : Type u'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : α → α') : (Stream'.Seq.map f s₁).zip s₂ = Stream'.Seq.map (Prod.map f id) (s₁.zip s₂)
• Stream'.Seq.zip_map_right 📋 Mathlib.Data.Seq.Basic
  {α : Type u} {β : Type v} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f : β → β') : s₁.zip (Stream'.Seq.map f s₂) = Stream'.Seq.map (Prod.map id f) (s₁.zip s₂)
• Stream'.Seq.enum_cons 📋 Mathlib.Data.Seq.Basic
  {α : Type u} (s : Stream'.Seq α) (x : α) : (Stream'.Seq.cons x s).enum = Stream'.Seq.cons (0, x) (Stream'.Seq.map (Prod.map Nat.succ id) s.enum)
• Stream'.Seq.zip_map 📋 Mathlib.Data.Seq.Basic
  {α : Type u} {β : Type v} {α' : Type u'} {β' : Type v'} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) (f₁ : α → α') (f₂ : β → β') : (Stream'.Seq.map f₁ s₁).zip (Stream'.Seq.map f₂ s₂) = Stream'.Seq.map (Prod.map f₁ f₂) (s₁.zip s₂)
• LieHom.coe_prodMap 📋 Mathlib.Algebra.Lie.Prod
  {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [CommRing R] [LieRing L₁] [LieAlgebra R L₁] [LieRing L₂] [LieAlgebra R L₂] [LieRing L₃] [LieAlgebra R L₃] [LieRing L₄] [LieAlgebra R L₄] (f : L₁ →ₗ⁅R⁆ L₃) (g : L₂ →ₗ⁅R⁆ L₄) : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
• Measurable.prodMap 📋 Mathlib.MeasureTheory.MeasurableSpace.Constructions
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} (hf : Measurable f) (hg : Measurable g) : Measurable (Prod.map f g)
• Metric.isBounded_range_of_tendsto_cofinite_uniformity 📋 Mathlib.Topology.MetricSpace.Bounded
  {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} (hf : Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (uniformity α)) : Bornology.IsBounded (Set.range f)
• AntilipschitzWith.comap_uniformity_le 📋 Mathlib.Topology.MetricSpace.Antilipschitz
  {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) : Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
• Isometry.prodMap 📋 Mathlib.Topology.MetricSpace.Isometry
  {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {δ : Type u_3} [PseudoEMetricSpace δ] {f : α → β} {g : γ → δ} (hf : Isometry f) (hg : Isometry g) : Isometry (Prod.map f g)
• ContinuousAlgHom.coe_prodMap' 📋 Mathlib.Topology.Algebra.Algebra
  {R : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [TopologicalSpace A] {B : Type u_3} [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B] {C : Type u_4} [Semiring C] [Algebra R C] [TopologicalSpace C] {D : Type u_5} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) : ⇑(f₁.prodMap f₂) = Prod.map ⇑f₁ ⇑f₂
• MeasurableSpace.comap_prodMap 📋 Mathlib.MeasureTheory.MeasurableSpace.Prod
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (X : γ → α) (Y : δ → β) : MeasurableSpace.comap (Prod.map X Y) (mα.prod mβ) = (MeasurableSpace.comap X mα).prod (MeasurableSpace.comap Y mβ)
• MeasurableEmbedding.prodMap 📋 Mathlib.MeasureTheory.MeasurableSpace.Prod
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β} {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) : MeasurableEmbedding (Prod.map g f)
• MeasureTheory.MeasurePreserving.prod 📋 Mathlib.MeasureTheory.Measure.Prod
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {δ : Type u_4} [MeasurableSpace δ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ} [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : α → β} {g : γ → δ} (hf : MeasureTheory.MeasurePreserving f μa μb) (hg : MeasureTheory.MeasurePreserving g μc μd) : MeasureTheory.MeasurePreserving (Prod.map f g) (μa.prod μc) (μb.prod μd)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision a114d38 serving mathlib revision 0d14bcb