Loogle!
Result
Found 1255 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.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.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₂) - 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 - DirectedOn.prod 📋 Mathlib.Order.Directed
{α : Type u} {β : Type v} {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.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.add_image_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Add α] {s t : Set α} : (fun x => x.1 + x.2) '' s ×ˢ t = s + t - Set.image_div_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Div α] {s t : Set α} : (fun x => x.1 / x.2) '' s ×ˢ t = s / t - Set.image_mul_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Mul α] {s t : Set α} : (fun x => x.1 * x.2) '' s ×ˢ t = s * t - Set.sub_image_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} [Sub α] {s t : Set α} : (fun x => x.1 - x.2) '' s ×ˢ t = s - t - Set.one_prod_one 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [One α] [One β] : 1 ×ˢ 1 = 1 - Set.zero_prod_zero 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Zero α] [Zero β] : 0 ×ˢ 0 = 0 - Set.inv_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Inv α] [Inv β] (s : Set α) (t : Set β) : (s ×ˢ t)⁻¹ = s⁻¹ ×ˢ t⁻¹ - Set.neg_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Neg α] [Neg β] (s : Set α) (t : Set β) : -s ×ˢ t = (-s) ×ˢ (-t) - Set.prod_add_prod_comm 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Add α] [Add β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) : s₁ ×ˢ t₁ + s₂ ×ˢ t₂ = (s₁ + s₂) ×ˢ (t₁ + t₂) - Set.prod_mul_prod_comm 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (s₁ s₂ : Set α) (t₁ t₂ : Set β) : s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂) - Set.nsmul_prod 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [AddMonoid α] [AddMonoid β] (s : Set α) (t : Set β) (n : ℕ) : n • s ×ˢ t = (n • s) ×ˢ (n • t) - Set.prod_pow 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
{α : Type u_2} {β : Type u_3} [Monoid α] [Monoid β] (s : Set α) (t : Set β) (n : ℕ) : s ×ˢ t ^ n = (s ^ n) ×ˢ (t ^ n) - 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 ×ˢ ∅ = ∅
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:
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 ?aIf 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 ?bBy 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 findtsum_lt_tsumeven though the hypothesisf i < g iis 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 6ff4759 serving mathlib revision 519f454