Loogle!

Result

Found 327 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')
• Prod.map.eq_1 📋 Init.Data.List.Zip
  {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂} (f : α₁ → α₂) (g : β₁ → β₂) (a' : α₁) (b' : β₁) : Prod.map f g (a', b') = (f a', g b')
• 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.enumFrom_eq_map_enum 📋 Init.Data.List.Range
  {α : Type u_1} (l : List α) (n : ℕ) : List.enumFrom n l = List.map (Prod.map (fun x => x + n) id) l.enum
• List.map_fst_add_enum_eq_enumFrom 📋 Init.Data.List.Range
  {α : Type u_1} (l : List α) (n : ℕ) : List.map (Prod.map (fun x => x + n) id) l.enum = List.enumFrom n l
• List.map_fst_add_enumFrom_eq_enumFrom 📋 Init.Data.List.Range
  {α : Type u_1} (l : List α) (n k : ℕ) : List.map (Prod.map (fun x => x + n) id) (List.enumFrom k l) = List.enumFrom (n + k) 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.enumFrom_cons' 📋 Init.Data.List.Range
  {α : Type u_1} (n : ℕ) (x : α) (xs : List α) : List.enumFrom n (x :: xs) = (n, x) :: List.map (Prod.map (fun x => x + 1) id) (List.enumFrom n xs)
• 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.enum_cons' 📋 Init.Data.List.Range
  {α : Type u_1} (x : α) (xs : List α) : (x :: xs).enum = (0, x) :: List.map (Prod.map (fun x => x + 1) id) xs.enum
• 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.enum_map 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β) : (List.map f l).enum = List.map (Prod.map id f) l.enum
• List.map_enum 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map (Prod.map id f) l.enum = (List.map f l).enum
• List.enumFrom_map 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} (n : ℕ) (l : List α) (f : α → β) : List.enumFrom n (List.map f l) = List.map (Prod.map id f) (List.enumFrom n l)
• List.map_enumFrom 📋 Init.Data.List.Nat.Range
  {α : Type u_1} {β : Type u_2} (f : α → β) (n : ℕ) (l : List α) : List.map (Prod.map id f) (List.enumFrom n l) = List.enumFrom n (List.map f l)
• 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.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} (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)
• Antitone.prod_map 📋 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)
• Monotone.prod_map 📋 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)
• StrictAnti.prod_map 📋 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)
• StrictMono.prod_map 📋 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)
• 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.range_prod_map 📋 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.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.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 β)
• Set.mapsTo_prod_map_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
• 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
• 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
• 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✝
• 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✝
• AddActionHom.prodMap.eq_1 📋 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 = { toFun := Prod.map ⇑f ⇑g, map_vadd' := ⋯ }
• MulActionHom.prodMap.eq_1 📋 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 = { toFun := Prod.map ⇑f ⇑g, map_smul' := ⋯ }
• 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
• 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
• 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
• 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
• 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)
• Finset.Nat.antidiagonal_succ' 📋 Mathlib.Data.Finset.NatAntidiagonal
  (n : ℕ) : Finset.antidiagonal (n + 1) = Finset.cons (n + 1, 0) (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯
• Finset.Nat.antidiagonal_succ 📋 Mathlib.Data.Finset.NatAntidiagonal
  (n : ℕ) : Finset.antidiagonal (n + 1) = Finset.cons (0, n + 1) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal n)) ⋯
• Finset.Nat.antidiagonal_succ_succ' 📋 Mathlib.Data.Finset.NatAntidiagonal
  {n : ℕ} : Finset.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯) ⋯
• 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
• Finsupp.antidiagonal'.eq_1 📋 Mathlib.Data.Finsupp.Antidiagonal
  {α : Type u} [DecidableEq α] (f : α →₀ ℕ) : f.antidiagonal' = Multiset.toFinsupp (Multiset.map (Prod.map ⇑Multiset.toFinsupp ⇑Multiset.toFinsupp) (Finsupp.toMultiset f).antidiagonal)
• 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.isFixedPt_prod_map 📋 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.isPeriodicPt_prod_map 📋 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)
• Function.minimalPeriod_prod_map 📋 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)
• Int.divisorsAntidiag_neg_natCast 📋 Mathlib.NumberTheory.Divisors
  (n : ℕ) : (-↑n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯
• Int.divisorsAntidiag_natCast 📋 Mathlib.NumberTheory.Divisors
  (n : ℕ) : (↑n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal) ⋯
• Int.divisorsAntidiag_ofNat 📋 Mathlib.NumberTheory.Divisors
  (n : ℕ) : (OfNat.ofNat n).divisorsAntidiag = (Finset.map (Nat.castEmbedding.prodMap Nat.castEmbedding) n.divisorsAntidiagonal).disjUnion (Finset.map ((Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ))).prodMap (Nat.castEmbedding.trans (Equiv.toEmbedding (Equiv.neg ℤ)))) n.divisorsAntidiagonal) ⋯
• 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.Tendsto.prod_map_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.map_prod_map_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.EventuallyEq.prod_map 📋 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.Tendsto.prod_map 📋 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.map_prod_map_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
• Filter.EventuallyLE.prod_map 📋 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)
• Inducing.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)
• 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.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₂
• 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)
• ContinuousOn.prod_map 📋 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)
• ContinuousWithinAt.prod_map 📋 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)
• 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.quotientMap_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
• 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✝
• 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)
• IsSymmetricRel.preimage_prodMap 📋 Mathlib.Topology.UniformSpace.Defs
  {α : Type ua} {β : Type ub} {U : Set (β × β)} (ht : IsSymmetricRel U) (f : α → β) : IsSymmetricRel (Prod.map f f ⁻¹' U)
• 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 : Set (β × β)} {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 : Set (α × α)} (ha : a ∈ uniformity α) {b : Set (β × β)} (hb : b ∈ uniformity β) : Prod.map Sum.inl Sum.inl '' a ∪ Prod.map Sum.inr Sum.inr '' b ∈ uniformity (α ⊕ β)
• 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.prod_map 📋 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
• 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')
• TendstoUniformly.prod_map 📋 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')
• UniformCauchySeqOn.prod_map 📋 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')
• TendstoUniformlyOn.prod_map 📋 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')
• TendstoUniformlyOnFilter.prod_map 📋 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')
• 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 α)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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.

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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65