Loogle!

Result

Found 1284 declarations mentioning SProd.sprod. Of these, only the first 200 are shown.

SProd.sprod 📋 Mathlib.Data.SProd
{α : Type u} {β : Type v} {γ : outParam (Type w)} [self : SProd α β γ] : α → β → γ
Set.prod_eq 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} (s : Set α) (t : Set β) : s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t
Set.mk_mem_prod 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} (ha : a ∈ s) (hb : b ∈ t) : (a, b) ∈ s ×ˢ t
Set.prodMk_mem_set_prod_eq 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β} : ((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)
Set.mem_prod 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
Set.mem_prod_eq 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β} : (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t)
Set.prod_image_left 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β) : (f '' s) ×ˢ t = (fun x => (f x.1, x.2)) '' s ×ˢ t
Set.prod_image_right 📋 Mathlib.Data.Set.Operations
{α : Type u} {β : Type v} {γ : Type w} (f : α → γ) (s : Set α) (t : Set β) : t ×ˢ (f '' s) = (fun x => (x.1, f x.2)) '' t ×ˢ s
Set.univ_prod_univ 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} : Set.univ ×ˢ Set.univ = Set.univ
Set.Nonempty.fst 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).Nonempty → s.Nonempty
Set.Nonempty.snd 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).Nonempty → t.Nonempty
Set.mapsTo_fst_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.MapsTo Prod.fst (s ×ˢ t) s
Set.mapsTo_snd_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.MapsTo Prod.snd (s ×ˢ t) t
Set.offDiag_subset_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s : Set α) : s.offDiag ⊆ s ×ˢ s
Set.Nonempty.prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
Set.Subsingleton.prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (hs : s.Subsingleton) (ht : t.Subsingleton) : (s ×ˢ t).Subsingleton
Set.diag_preimage_prod_self 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s
Set.prod_nonempty_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Set.prod_univ 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} : s ×ˢ Set.univ = Prod.fst ⁻¹' s
Set.univ_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {t : Set β} : Set.univ ×ˢ t = Prod.snd ⁻¹' t
Set.fst_image_prod_subset 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.fst '' s ×ˢ t ⊆ s
Set.snd_image_prod_subset 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.snd '' s ×ˢ t ⊆ t
Set.fst_image_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set β) {t : Set α} (ht : t.Nonempty) : Prod.fst '' s ×ˢ t = s
Set.snd_image_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) (t : Set β) : Prod.snd '' s ×ˢ t = t
Set.empty_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {t : Set β} : ∅ ×ˢ t = ∅
Set.prod_empty 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} : s ×ˢ ∅ = ∅
Set.prod_sdiff_diagonal 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s : Set α) : s ×ˢ s \ Set.diagonal α = s.offDiag
Set.prod_subset_preimage_fst 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.fst ⁻¹' s
Set.prod_subset_preimage_snd 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.snd ⁻¹' t
Set.diag_preimage_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t
Set.singleton_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {t : Set β} {a : α} : {a} ×ˢ t = Prod.mk a '' t
Set.mk_preimage_prod_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a ∈ s) : Prod.mk a ⁻¹' s ×ˢ t = t
Set.prod_singleton 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {b : β} : s ×ˢ {b} = (fun a => (a, b)) '' s
Set.mapsTo_swap_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Set.MapsTo Prod.swap (s ×ˢ t) (t ×ˢ s)
Set.mk_preimage_prod_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b ∈ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = s
Set.diag_image 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s : Set α) : (fun x => (x, x)) '' s = Set.diagonal α ∩ s ×ˢ s
Set.subset_fst_image_prod_snd_image 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set (α × β)} : s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
Set.subset_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set (α × β)} : s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
Set.mk_preimage_prod_right_eq_empty 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a ∉ s) : Prod.mk a ⁻¹' s ×ˢ t = ∅
Set.prod_eq_univ 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty α] [Nonempty β] : s ×ˢ t = Set.univ ↔ s = Set.univ ∧ t = Set.univ
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.image_prodMk_subset_prod_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} (ha : a ∈ s) : Prod.mk a '' t ⊆ s ×ˢ t
Set.image_swap_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.swap '' s ×ˢ t = t ×ˢ s
Set.mk_preimage_prod_left_eq_empty 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b ∉ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
Set.preimage_swap_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
Set.range_pair_subset 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : α → γ) : (Set.range fun x => (f x, g x)) ⊆ Set.range f ×ˢ Set.range g
Set.image_prodMk_subset_prod_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} (hb : b ∈ t) : (fun a => (a, b)) '' s ⊆ s ×ˢ t
Set.prod_eq_iff_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} (ht : t.Nonempty) : s ×ˢ t = s₁ ×ˢ t ↔ s = s₁
Set.prod_range_univ_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {m₁ : α → γ} : Set.range m₁ ×ˢ Set.univ = Set.range fun p => (m₁ p.1, p.2)
Set.prod_self_ssubset_prod_self 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {s₁ s₂ : Set α} : s₁ ×ˢ s₁ ⊂ s₂ ×ˢ s₂ ↔ s₁ ⊂ s₂
Set.prod_self_subset_prod_self 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {s₁ s₂ : Set α} : s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂
Set.prod_univ_range_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {δ : Type u_4} {m₂ : β → δ} : Set.univ ×ˢ Set.range m₂ = Set.range fun p => (p.1, m₂ p.2)
Set.prod_mono_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} (hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t
Set.prod_mono_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂
Set.prod_subset_prod_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} (hs : s₁ ⊆ s₂) : s₁ ×ˢ t ⊆ s₂ ×ˢ t
Set.prod_subset_prod_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} (ht : t₁ ⊆ t₂) : s ×ˢ t₁ ⊆ s ×ˢ t₂
Set.singleton_prod_singleton 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {a : α} {b : β} : {a} ×ˢ {b} = {(a, b)}
Set.image_prodMk_subset_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {s : Set α} : (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s)
Set.prod_eq_empty_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
Set.mk_preimage_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : γ → α) (g : γ → β) : (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t
Set.offDiag_eq_sep_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} (s : Set α) : s.offDiag = {x | x ∈ s ×ˢ s ∧ x.1 ≠ x.2}
Set.prod_range_range_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ} : Set.range m₁ ×ˢ Set.range m₂ = Set.range fun p => (m₁ p.1, m₂ p.2)
Set.prod_subset_prod_iff_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t : Set β} (h : t.Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t ↔ s ⊆ s₁
Set.prod_subset_prod_iff_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t t₁ : Set β} (h : s.Nonempty) : s ×ˢ t ⊆ s ×ˢ t₁ ↔ t ⊆ t₁
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.prod_mono 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂
Set.decidableMemProd 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [DecidablePred fun x => x ∈ s] [DecidablePred fun x => x ∈ t] : DecidablePred fun x => x ∈ s ×ˢ t
Set.mk_preimage_prod_right_eq_if 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} [DecidablePred fun x => x ∈ s] : Prod.mk a ⁻¹' s ×ˢ t = if a ∈ s then t else ∅
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.mk_preimage_prod_left_eq_if 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} [DecidablePred fun x => x ∈ t] : (fun a => (a, b)) ⁻¹' s ×ˢ t = if b ∈ t then s else ∅
Set.insert_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α} : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t
Set.forall_prod_set 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop} : (∀ x ∈ s ×ˢ t, p x) ↔ ∀ x ∈ s, ∀ y ∈ t, p (x, y)
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.prod_insert 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β} : s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t
Set.prod_preimage_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : γ → α} : (f ⁻¹' s) ×ˢ t = (fun p => (f p.1, p.2)) ⁻¹' s ×ˢ t
Set.prod_preimage_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {g : δ → β} : s ×ˢ (g ⁻¹' t) = (fun p => (p.1, g p.2)) ⁻¹' s ×ˢ t
Set.inter_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} : (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
Set.prod_inter 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
Set.prod_union 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β} : s ×ˢ (t₁ ∪ t₂) = s ×ˢ t₁ ∪ s ×ˢ t₂
Set.union_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β} : (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
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.prod_subset_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {P : Set (α × β)} : s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P
Set.uncurry_preimage_prod_pi 📋 Mathlib.Data.Set.Prod
{ι : Type u_1} {κ : Type u_4} {α : Type u_5} (s : Set ι) (t : Set κ) (u : ι × κ → Set α) : Function.uncurry ⁻¹' (s ×ˢ t).pi u = s.pi fun i => t.pi fun j => u (i, j)
Set.mk_preimage_prod_left_fn_eq_if 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {b : β} [DecidablePred fun x => x ∈ t] (f : γ → α) : (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
Set.mk_preimage_prod_right_fn_eq_if 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {δ : Type u_4} {s : Set α} {t : Set β} {a : α} [DecidablePred fun x => x ∈ s] (g : δ → β) : (fun b => (a, g b)) ⁻¹' s ×ˢ t = if a ∈ s then g ⁻¹' t else ∅
Set.prod_eq_prod_iff_of_nonempty 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} (h : (s ×ˢ t).Nonempty) : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁
Set.prod_sub_preimage_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {W : Set γ} {f : α × β → γ} : s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W
Set.prod_image_image_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {m₁ : α → γ} {m₂ : β → δ} : (m₁ '' s) ×ˢ (m₂ '' t) = (fun p => (m₁ p.1, m₂ p.2)) '' s ×ˢ t
Set.prod_preimage_eq 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {s : Set α} {t : Set β} {f : γ → α} {g : δ → β} : (f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p => (f p.1, g p.2)) ⁻¹' s ×ˢ t
Set.prod_subset_compl_diagonal_iff_disjoint 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {s t : Set α} : s ×ˢ t ⊆ (Set.diagonal α)ᶜ ↔ Disjoint s t
Set.exists_prod_set 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {p : α × β → Prop} : (∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)
Set.prod_inter_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
Set.prod_subset_prod_iff' 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} (h : (s ×ˢ t).Nonempty) : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁
Set.compl_prod_eq_union 📋 Mathlib.Data.Set.Prod
{α : Type u_5} {β : Type u_6} (s : Set α) (t : Set β) : (s ×ˢ t)ᶜ = sᶜ ×ˢ Set.univ ∪ Set.univ ×ˢ tᶜ
Set.prod_subset_prod_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} : s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
image_toPullbackDiag 📋 Mathlib.Data.Set.Prod
{X : Type u_1} {Y : Sort u_2} (f : X → Y) (s : Set X) : toPullbackDiag f '' s = Function.pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s
Set.offDiag_insert 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}
Set.prod_eq_prod_iff 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} : s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
Set.prod_diff_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
Set.prod_sdiff_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β} : s ×ˢ t \ s₁ ×ˢ t₁ = s ×ˢ (t \ t₁) ∪ (s \ s₁) ×ˢ t
Set.offDiag_union 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {s t : Set α} (h : Disjoint s t) : (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s
Antitone.set_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : Antitone f) (hg : Antitone g) : Antitone fun x => f x ×ˢ g x
Monotone.set_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : Monotone f) (hg : Monotone g) : Monotone fun x => f x ×ˢ g x
Set.Disjoint.set_prod_left 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} (hs : Disjoint s₁ s₂) (t₁ t₂ : Set β) : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
Set.Disjoint.set_prod_right 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {t₁ t₂ : Set β} (ht : Disjoint t₁ t₂) (s₁ s₂ : Set α) : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂)
AntitoneOn.set_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (fun x => f x ×ˢ g x) s
MonotoneOn.set_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} [Preorder α] {f : α → Set β} {g : α → Set γ} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (fun x => f x ×ˢ g x) s
Set.disjoint_prod 📋 Mathlib.Data.Set.Prod
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ 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
Equiv.sumPiEquivProdPi_symm_preimage_univ_pi 📋 Mathlib.Data.Set.Prod
{ι : Type u_1} {ι' : Type u_2} (π : ι ⊕ ι' → Type u_4) (t : (i : ι ⊕ ι') → Set (π i)) : ⇑(Equiv.sumPiEquivProdPi π).symm ⁻¹' Set.univ.pi t = (Set.univ.pi fun i => t (Sum.inl i)) ×ˢ Set.univ.pi fun i => t (Sum.inr i)
Set.prod_surjOn_fst 📋 Mathlib.Data.Set.Function
{β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂} (h : t₂.Nonempty) : Set.SurjOn Prod.fst (t₁ ×ˢ t₂) t₁
Set.prod_surjOn_snd 📋 Mathlib.Data.Set.Function
{β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂} (h : t₁.Nonempty) : Set.SurjOn Prod.snd (t₁ ×ˢ t₂) t₂
Set.prod_surjOn_fst_iff 📋 Mathlib.Data.Set.Function
{β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂} : Set.SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ↔ t₁ = ∅ ∨ t₂.Nonempty
Set.prod_surjOn_snd_iff 📋 Mathlib.Data.Set.Function
{β₁ : Type u_8} {β₂ : Type u_9} {t₁ : Set β₁} {t₂ : Set β₂} : Set.SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ↔ t₁.Nonempty ∨ t₂ = ∅
Set.MapsTo.prodMk 📋 Mathlib.Data.Set.Function
{α : Type u_7} {β₁ : Type u_8} {β₂ : Type u_9} {s : Set α} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α → β₁} {f₂ : α → β₂} (h₁ : Set.MapsTo f₁ s t₁) (h₂ : Set.MapsTo f₂ s t₂) : Set.MapsTo (fun x => (f₁ x, f₂ x)) s (t₁ ×ˢ t₂)
Set.InjOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} (h₁ : Set.InjOn f₁ s₁) (h₂ : Set.InjOn f₂ s₂) : Set.InjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
Set.BijOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} (h₁ : Set.BijOn f₁ s₁ t₁) (h₂ : Set.BijOn f₂ s₂ t₂) : Set.BijOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
Set.MapsTo.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} (h₁ : Set.MapsTo f₁ s₁ t₁) (h₂ : Set.MapsTo f₂ s₂ t₂) : Set.MapsTo (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
Set.SurjOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} (h₁ : Set.SurjOn f₁ s₁ t₁) (h₂ : Set.SurjOn f₂ s₂ t₂) : Set.SurjOn (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
Set.LeftInvOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂} (h₁ : Set.LeftInvOn g₁ f₁ s₁) (h₂ : Set.LeftInvOn g₂ f₂ s₂) : Set.LeftInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)
Set.RightInvOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂} (h₁ : Set.RightInvOn g₁ f₁ t₁) (h₂ : Set.RightInvOn g₂ f₂ t₂) : Set.RightInvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)
Set.InvOn.prodMap 📋 Mathlib.Data.Set.Function
{α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂} (h₁ : Set.InvOn g₁ f₁ s₁ t₁) (h₂ : Set.InvOn g₂ f₂ s₂ t₂) : Set.InvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)
DirectedOn.prod 📋 Mathlib.Order.Directed
{α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r₂ : β → β → Prop} {d₁ : Set α} {d₂ : Set β} (h₁ : DirectedOn (fun x1 x2 => r x1 x2) d₁) (h₂ : DirectedOn (fun x1 x2 => r₂ x1 x2) d₂) : DirectedOn (fun p q => r p.1 q.1 ∧ r₂ p.2 q.2) (d₁ ×ˢ d₂)
Set.image2_mk_eq_prod 📋 Mathlib.Data.Set.NAry
{α : Type u_1} {β : Type u_3} {s : Set α} {t : Set β} : Set.image2 Prod.mk s t = s ×ˢ t
Set.image_uncurry_prod 📋 Mathlib.Data.Set.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) (s : Set α) (t : Set β) : Function.uncurry f '' s ×ˢ t = Set.image2 f s t
Set.image2_curry 📋 Mathlib.Data.Set.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α × β → γ) (s : Set α) (t : Set β) : Set.image2 (fun a b => f (a, b)) s t = f '' s ×ˢ t
Set.image_prod 📋 Mathlib.Data.Set.NAry
{α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) {s : Set α} {t : Set β} : (fun x => f x.1 x.2) '' s ×ˢ t = Set.image2 f s t
Set.Ici_prod_Ici 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Set.Ici a ×ˢ Set.Ici b = Set.Ici (a, b)
Set.Iic_prod_Iic 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α) (b : β) : Set.Iic a ×ˢ Set.Iic b = Set.Iic (a, b)
Set.Ici_prod_eq 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Set.Ici a = Set.Ici a.1 ×ˢ Set.Ici a.2
Set.Iic_prod_eq 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a : α × β) : Set.Iic a = Set.Iic a.1 ×ˢ Set.Iic a.2
Set.Icc_prod_Icc 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) : Set.Icc a₁ a₂ ×ˢ Set.Icc b₁ b₂ = Set.Icc (a₁, b₁) (a₂, b₂)
Set.Icc_prod_eq 📋 Mathlib.Order.Interval.Set.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (a b : α × β) : Set.Icc a b = Set.Icc a.1 b.1 ×ˢ Set.Icc a.2 b.2
IsGLB.prod 📋 Mathlib.Order.Bounds.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsGLB s a) (hb : IsGLB t b) : IsGLB (s ×ˢ t) (a, b)
IsLUB.prod 📋 Mathlib.Order.Bounds.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} {a : α} {b : β} (hs : s.Nonempty) (ht : t.Nonempty) (ha : IsLUB s a) (hb : IsLUB t b) : IsLUB (s ×ˢ t) (a, b)
lowerBounds_prod 📋 Mathlib.Order.Bounds.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : lowerBounds (s ×ˢ t) = lowerBounds s ×ˢ lowerBounds t
upperBounds_prod 📋 Mathlib.Order.Bounds.Basic
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t
DirectedOn.isCofinalFor_fst_image_prod_snd_image 📋 Mathlib.Order.Bounds.Basic
{α : Type u_1} [Preorder α] {β : Type u_4} [Preorder β] {s : Set (α × β)} (hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s) : IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s
Monotone.upperBounds_image_of_directedOn_prod 📋 Mathlib.Order.Bounds.Image
{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {γ : Type u_3} [Preorder γ] {g : α × β → γ} (hg : Monotone g) {d : Set (α × β)} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) d) : upperBounds (g '' d) = upperBounds (g '' (Prod.fst '' d) ×ˢ (Prod.snd '' d))
Equiv.Set.prod 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : Type u_4} (s : Set α) (t : Set β) : ↑(s ×ˢ t) ≃ ↑s × ↑t
Equiv.prod_assoc_image 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(Equiv.prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
Equiv.prod_assoc_preimage 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(Equiv.prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
Equiv.prod_assoc_symm_image 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
Equiv.prod_assoc_symm_preimage 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ} : ⇑(Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
Equiv.preimage_piEquivPiSubtypeProd_symm_pi 📋 Mathlib.Logic.Equiv.Set
{α : Type u_3} {β : α → Type u_4} (p : α → Prop) [DecidablePred p] (s : (i : α) → Set (β i)) : ⇑(Equiv.piEquivPiSubtypeProd p β).symm ⁻¹' Set.univ.pi s = (Set.univ.pi fun i => s ↑i) ×ˢ Set.univ.pi fun i => s ↑i
sInf_prod 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : sInf (s ×ˢ t) = (sInf s, sInf t)
sSup_prod 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) : sSup (s ×ˢ t) = (sSup s, sSup t)
biInf_prod 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : ⨅ x ∈ s ×ˢ t, f x = ⨅ a ∈ s, ⨅ b ∈ t, f (a, b)
biSup_prod 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ} : ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
biInf_prod' 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : ⨅ x ∈ s ×ˢ t, f x.1 x.2 = ⨅ a ∈ s, ⨅ b ∈ t, f a b
biSup_prod' 📋 Mathlib.Order.CompleteLattice.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [CompleteLattice α] {f : β → γ → α} {s : Set β} {t : Set γ} : ⨆ x ∈ s ×ˢ t, f x.1 x.2 = ⨆ a ∈ s, ⨆ b ∈ t, f a b
sInf_sup_sInf 📋 Mathlib.Order.CompleteBooleanAlgebra
{α : Type u} [Order.Coframe α] {s t : Set α} : sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, p.1 ⊔ p.2
sSup_inf_sSup 📋 Mathlib.Order.CompleteBooleanAlgebra
{α : Type u} [Order.Frame α] {s t : Set α} : sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2
biInf_sup_biInf 📋 Mathlib.Order.CompleteBooleanAlgebra
{α : Type u} [Order.Coframe α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} : (⨅ i ∈ s, f i) ⊔ ⨅ j ∈ t, g j = ⨅ p ∈ s ×ˢ t, f p.1 ⊔ g p.2
biSup_inf_biSup 📋 Mathlib.Order.CompleteBooleanAlgebra
{α : Type u} [Order.Frame α] {ι : Type u_1} {ι' : Type u_2} {f : ι → α} {g : ι' → α} {s : Set ι} {t : Set ι'} : (⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2
Set.sInter_union_sInter 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {S T : Set (Set α)} : ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, p.1 ∪ p.2
Set.sUnion_inter_sUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s t : Set (Set α)} : ⋃₀ s ∩ ⋃₀ t = ⋃ p ∈ s ×ˢ t, p.1 ∩ p.2
Set.uIcc_prod_uIcc 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a₁ a₂ : α) (b₁ b₂ : β) : Set.uIcc a₁ a₂ ×ˢ Set.uIcc b₁ b₂ = Set.uIcc (a₁, b₁) (a₂, b₂)
Set.uIcc_prod_eq 📋 Mathlib.Order.Interval.Set.UnorderedInterval
{α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] (a b : α × β) : Set.uIcc a b = Set.uIcc a.1 b.1 ×ˢ Set.uIcc a.2 b.2
Set.pairwiseDisjoint_image_right_iff 📋 Mathlib.Data.Set.Pairwise.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (hf : ∀ a ∈ s, Function.Injective (f a)) : (s.PairwiseDisjoint fun a => f a '' t) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t)
Set.pairwiseDisjoint_image_left_iff 📋 Mathlib.Data.Set.Pairwise.Basic
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : Set α} {t : Set β} (hf : ∀ b ∈ t, Function.Injective fun a => f a b) : (t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ Set.InjOn (fun p => f p.1 p.2) (s ×ˢ t)
Set.PairwiseDisjoint.prod 📋 Mathlib.Data.Set.Pairwise.Basic
{α : Type u_1} {β : Type u_2} {ι : Type u_4} {ι' : Type u_5} {s : Set ι} {t : Set ι'} {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint g) : (s ×ˢ t).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2
Set.image_sdiv_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Scalar
{α : Type u_2} {β : Type u_3} [SDiv α β] {s t : Set β} : (fun x => x.1 /ₛ x.2) '' s ×ˢ t = s /ₛ t
Set.image_vsub_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Scalar
{α : Type u_2} {β : Type u_3} [VSub α β] {s t : Set β} : (fun x => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t
Set.image_smul_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Scalar
{α : Type u_2} {β : Type u_3} [SMul α β] {s : Set α} {t : Set β} : (fun x => x.1 • x.2) '' s ×ˢ t = s • t
Set.vadd_image_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Scalar
{α : Type u_2} {β : Type u_3} [VAdd α β] {s : Set α} {t : Set β} : (fun x => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t
List.Nodup.product 📋 Mathlib.Data.List.Nodup
{α : Type u} {β : Type v} {l₁ : List α} {l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : (l₁ ×ˢ l₂).Nodup
List.nil_product 📋 Mathlib.Data.List.ProdSigma
{α : Type u_1} {β : Type u_2} (l : List β) : [] ×ˢ l = []
List.product_nil 📋 Mathlib.Data.List.ProdSigma
{α : Type u_1} {β : Type u_2} (l : List α) : l ×ˢ [] = []
List.length_product 📋 Mathlib.Data.List.ProdSigma
{α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β) : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
List.mem_product 📋 Mathlib.Data.List.ProdSigma
{α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {a : α} {b : β} : (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
List.product_cons 📋 Mathlib.Data.List.ProdSigma
{α : Type u_1} {β : Type u_2} (a : α) (l₁ : List α) (l₂ : List β) : (a :: l₁) ×ˢ l₂ = List.map (fun b => (a, b)) l₂ ++ l₁ ×ˢ l₂
Multiset.Nodup.product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} : s.Nodup → t.Nodup → (s ×ˢ t).Nodup
Multiset.card_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) : (s ×ˢ t).card = s.card * t.card
Multiset.product_zero 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (s : Multiset α) : s ×ˢ 0 = 0
Multiset.zero_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (t : Multiset β) : 0 ×ˢ t = 0
Multiset.coe_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (l₁ : List α) (l₂ : List β) : ↑l₁ ×ˢ ↑l₂ = ↑(l₁ ×ˢ l₂)
Multiset.map_swap_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β) : Multiset.map Prod.swap (s ×ˢ t) = t ×ˢ s
Multiset.product_singleton 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (a : α) (b : β) : {a} ×ˢ {b} = {(a, b)}
Multiset.mem_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} {s : Multiset α} {t : Multiset β} {p : α × β} : p ∈ s ×ˢ t ↔ p.1 ∈ s ∧ p.2 ∈ t
Multiset.prod_map_product_eq_prod_prod 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} {M : Type u_4} [CommMonoid M] (s : Multiset α) (t : Multiset β) (f : α × β → M) : (Multiset.map f (s ×ˢ t)).prod = (Multiset.map (fun i => (Multiset.map (fun j => f (i, j)) t).prod) s).prod
Multiset.cons_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (a : α) (s : Multiset α) (t : Multiset β) : (a ::ₘ s) ×ˢ t = Multiset.map (Prod.mk a) t + s ×ˢ t
Multiset.product_cons 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (b : β) (s : Multiset α) (t : Multiset β) : s ×ˢ (b ::ₘ t) = Multiset.map (fun a => (a, b)) s + s ×ˢ t
Multiset.add_product 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (s t : Multiset α) (u : Multiset β) : (s + t) ×ˢ u = s ×ˢ u + t ×ˢ u
Multiset.product_add 📋 Mathlib.Data.Multiset.Bind
{α : Type u_1} {β : Type v} (s : Multiset α) (t u : Multiset β) : s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
Finset.Nonempty.fst 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : (s ×ˢ t).Nonempty) : s.Nonempty
Finset.Nonempty.snd 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : (s ×ˢ t).Nonempty) : t.Nonempty
Finset.product_eq_sprod 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : s.product t = s ×ˢ t
Finset.Nonempty.product 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (hs : s.Nonempty) (ht : t.Nonempty) : (s ×ˢ t).Nonempty
Finset.nonempty_product 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
Finset.empty_product 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} (t : Finset β) : ∅ ×ˢ t = ∅
Finset.product_empty 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} (s : Finset α) : s ×ˢ ∅ = ∅
Finset.subset_product_image_fst 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] : Finset.image Prod.fst (s ×ˢ t) ⊆ s
Finset.subset_product_image_snd 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] : Finset.image Prod.snd (s ×ˢ t) ⊆ t
Finset.product_image_fst 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] (ht : t.Nonempty) : Finset.image Prod.fst (s ×ˢ t) = s
Finset.product_image_snd 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] (ht : s.Nonempty) : Finset.image Prod.snd (s ×ˢ t) = t
Finset.card_product 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) : (s ×ˢ t).card = s.card * t.card

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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.
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 e568743