Loogle!

Result

Found 958 declarations mentioning Disjoint and Set. Of these, 842 match your pattern(s). Of these, only the first 200 are shown.

• Set.disjoint_empty 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} (s : Set α) : Disjoint s ∅
• Set.empty_disjoint 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} (s : Set α) : Disjoint ∅ s
• Set.disjoint_univ 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s : Set α} : Disjoint s Set.univ ↔ s = ∅
• Set.univ_disjoint 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s : Set α} : Disjoint Set.univ s ↔ s = ∅
• Set.disjoint_or_nonempty_inter 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} (s t : Set α) : Disjoint s t ∨ (s ∩ t).Nonempty
• Set.Nonempty.not_disjoint 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : (s ∩ t).Nonempty → ¬Disjoint s t
• Set.not_disjoint_iff_nonempty_inter 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : ¬Disjoint s t ↔ (s ∩ t).Nonempty
• Disjoint.inter_eq 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t → s ∩ t = ∅
• Set.disjoint_iff_inter_eq_empty 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t ↔ s ∩ t = ∅
• Set.disjoint_range_iff 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {β : Sort u_1} {γ : Sort u_2} {x : β → α} {y : γ → α} : Disjoint (Set.range x) (Set.range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j
• Disjoint.notMem_of_mem_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → a ∉ t
• Disjoint.notMem_of_mem_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ t → a ∉ s
• Set.disjoint_iff 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t ↔ s ∩ t ⊆ ∅
• Set.disjoint_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
• Set.disjoint_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
• Disjoint.ne_of_mem 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
• Disjoint.subset_left_of_subset_union 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t
• Disjoint.subset_right_of_subset_union 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t u : Set α} (h : s ⊆ t ∪ u) (hab : Disjoint s t) : s ⊆ u
• Set.not_disjoint_iff 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : ¬Disjoint s t ↔ ∃ x ∈ s, x ∈ t
• Set.disjoint_iff_forall_ne 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t : Set α} : Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
• Set.mem_union_of_disjoint 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) {x : α} : x ∈ s ∪ t ↔ Xor' (x ∈ s) (x ∈ t)
• Disjoint.inter_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint (s ∩ u) t
• Disjoint.inter_left' 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint (u ∩ s) t
• Disjoint.inter_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint s (t ∩ u)
• Disjoint.inter_right' 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t : Set α} (u : Set α) (h : Disjoint s t) : Disjoint s (u ∩ t)
• Set.disjoint_of_subset_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t u : Set α} (h : s ⊆ u) (d : Disjoint u t) : Disjoint s t
• Set.disjoint_of_subset_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t u : Set α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t
• Set.disjoint_of_subset 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s₁ s₂ t₁ t₂ : Set α} (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) (h : Disjoint s₂ t₂) : Disjoint s₁ t₁
• Disjoint.union_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t u : Set α} (hs : Disjoint s u) (ht : Disjoint t u) : Disjoint (s ∪ t) u
• Disjoint.union_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u_1} {s t u : Set α} (ht : Disjoint s t) (hu : Disjoint s u) : Disjoint s (t ∪ u)
• Set.disjoint_union_left 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t u : Set α} : Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
• Set.disjoint_union_right 📋 Mathlib.Data.Set.Disjoint
  {α : Type u} {s t u : Set α} : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
• Set.disjoint_singleton 📋 Mathlib.Data.Set.Insert
  {α : Type u} {a b : α} : Disjoint {a} {b} ↔ a ≠ b
• Set.disjoint_singleton_left 📋 Mathlib.Data.Set.Insert
  {α : Type u} {s : Set α} {a : α} : Disjoint {a} s ↔ a ∉ s
• Set.disjoint_singleton_right 📋 Mathlib.Data.Set.Insert
  {α : Type u} {s : Set α} {a : α} : Disjoint s {a} ↔ a ∉ s
• Set.disjoint_insert_left 📋 Mathlib.Data.Set.Insert
  {α : Type u} {s t : Set α} {a : α} : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
• Set.disjoint_insert_right 📋 Mathlib.Data.Set.Insert
  {α : Type u} {s t : Set α} {a : α} : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
• Set.disjoint_sdiff_left 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint (t \ s) s
• Set.disjoint_sdiff_right 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint s (t \ s)
• Disjoint.subset_compl_left 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint t s → s ⊆ tᶜ
• Disjoint.subset_compl_right 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint s t → s ⊆ tᶜ
• Set.disjoint_sdiff_inter 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint (s \ t) (s ∩ t)
• HasSubset.Subset.disjoint_compl_left 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : t ⊆ s → Disjoint sᶜ t
• HasSubset.Subset.disjoint_compl_right 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : s ⊆ t → Disjoint s tᶜ
• Set.disjoint_compl_left_iff_subset 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint sᶜ t ↔ t ⊆ s
• Set.disjoint_compl_right_iff_subset 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : Disjoint s tᶜ ↔ s ⊆ t
• Set.subset_compl_iff_disjoint_left 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint t s
• Set.subset_compl_iff_disjoint_right 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} : s ⊆ tᶜ ↔ Disjoint s t
• Set.disjoint_of_subset_iff_left_eq_empty 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t : Set α} (h : s ⊆ t) : Disjoint s t ↔ s = ∅
• Set.subset_diff 📋 Mathlib.Order.BooleanAlgebra.Set
  {α : Type u_1} {s t u : Set α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
• Set.subset_symmDiff_union_symmDiff_left 📋 Mathlib.Data.Set.SymmDiff
  {α : Type u} {s t u : Set α} (h : Disjoint s t) : u ⊆ symmDiff s u ∪ symmDiff t u
• Set.subset_symmDiff_union_symmDiff_right 📋 Mathlib.Data.Set.SymmDiff
  {α : Type u} {s t u : Set α} (h : Disjoint t u) : s ⊆ symmDiff s t ∪ symmDiff s u
• Set.preimage_eq_empty 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} (h : Disjoint s (Set.range f)) : f ⁻¹' s = ∅
• Set.preimage_eq_empty_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (Set.range f)
• Set.disjoint_powerset_insert 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {s : Set α} {a : α} (h : a ∉ s) : Disjoint (𝒫 s) (insert a '' 𝒫 s)
• Set.disjoint_image_image 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : β → α} {g : γ → α} {s : Set β} {t : Set γ} (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) : Disjoint (f '' s) (g '' t)
• Set.disjoint_image_inl_range_inr 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {u : Set α} : Disjoint (Sum.inl '' u) (Set.range Sum.inr)
• Set.disjoint_range_inl_image_inr 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {v : Set β} : Disjoint (Set.range Sum.inl) (Sum.inr '' v)
• Set.disjoint_image_inl_image_inr 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {u : Set α} {v : Set β} : Disjoint (Sum.inl '' u) (Sum.inr '' v)
• Disjoint.of_image 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α} (h : Disjoint (f '' s) (f '' t)) : Disjoint s t
• Disjoint.preimage 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} (f : α → β) {s t : Set β} (h : Disjoint s t) : Disjoint (f ⁻¹' s) (f ⁻¹' t)
• Set.disjoint_image_left 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
• Set.disjoint_image_right 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α} {t : Set β} : Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s
• Disjoint.of_preimage 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) {s t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) : Disjoint s t
• Set.disjoint_image_of_injective 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) {s t : Set α} (hd : Disjoint s t) : Disjoint (f '' s) (f '' t)
• Set.disjoint_image_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α} (hf : Function.Injective f) : Disjoint (f '' s) (f '' t) ↔ Disjoint s t
• Set.disjoint_preimage_iff 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Surjective f) {s t : Set β} : Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t
• Set.disjoint_diagonal_offDiag 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} (s : Set α) : Disjoint (Set.diagonal α) s.offDiag
• 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.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
• 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₂)
• Set.disjoint_univ_pi 📋 Mathlib.Data.Set.Prod
  {ι : Type u_1} {α : ι → Type u_2} {t₁ t₂ : (i : ι) → Set (α i)} : Disjoint (Set.univ.pi t₁) (Set.univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)
• Set.Disjoint.set_pi 📋 Mathlib.Data.Set.Prod
  {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} {i : ι} (hi : i ∈ s) (ht : Disjoint (t₁ i) (t₂ i)) : Disjoint (s.pi t₁) (s.pi t₂)
• Set.disjoint_pi 📋 Mathlib.Data.Set.Prod
  {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} [∀ (i : ι), Nonempty (α i)] : Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i ∈ s, Disjoint (t₁ i) (t₂ i)
• 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.injOn_union 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f : α → β} (h : Disjoint s₁ s₂) : Set.InjOn f (s₁ ∪ s₂) ↔ Set.InjOn f s₁ ∧ Set.InjOn f s₂ ∧ ∀ x ∈ s₁, ∀ y ∈ s₂, f x ≠ f y
• Disjoint.image 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} {s t u : Set α} {f : α → β} (h : Disjoint s t) (hf : Set.InjOn f u) (hs : s ⊆ u) (ht : t ⊆ u) : Disjoint (f '' s) (f '' t)
• Equiv.Set.union 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) : ↑(s ∪ t) ≃ ↑s ⊕ ↑t
• Equiv.Set.union_symm_apply_left 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : ↑s) : (Equiv.Set.union H).symm (Sum.inl a) = ⟨↑a, ⋯⟩
• Equiv.Set.union_symm_apply_right 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) (a : ↑t) : (Equiv.Set.union H).symm (Sum.inr a) = ⟨↑a, ⋯⟩
• Equiv.Set.union_apply_left 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ s) : (Equiv.Set.union H) a = Sum.inl ⟨↑a, ha⟩
• Equiv.Set.union_apply_right 📋 Mathlib.Logic.Equiv.Set
  {α : Type u_3} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t) {a : ↑(s ∪ t)} (ha : ↑a ∈ t) : (Equiv.Set.union H) a = Sum.inr ⟨↑a, ha⟩
• disjoint_of_sSup_disjoint 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a b : Set α} (hd : Disjoint (sSup a) (sSup b)) (he : ⊥ ∉ a ∨ ⊥ ∉ b) : Disjoint a b
• disjoint_of_sSup_disjoint_of_le_of_le 📋 Mathlib.Order.CompleteLattice.Lemmas
  {α : Type u_1} [CompleteLattice α] {a b : α} {c d : Set α} (hs : ∀ e ∈ c, e ≤ a) (ht : ∀ e ∈ d, e ≤ b) (hd : Disjoint a b) (he : ⊥ ∉ c ∨ ⊥ ∉ d) : Disjoint c d
• Set.unionEqSigmaOfDisjoint 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {β : Type u_2} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) : ↑(⋃ i, t i) ≃ (i : α) × ↑(t i)
• Set.sigmaToiUnion_bijective 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : Pairwise (Function.onFun Disjoint t)) : Function.Bijective (Set.sigmaToiUnion t)
• Set.sigmaToiUnion_injective 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : Pairwise (Function.onFun Disjoint t)) : Function.Injective (Set.sigmaToiUnion t)
• Set.disjoint_iUnion_left 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {t : Set α} {ι : Sort u_12} {s : ι → Set α} : Disjoint (⋃ i, s i) t ↔ ∀ (i : ι), Disjoint (s i) t
• Set.disjoint_iUnion_right 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {t : Set α} {ι : Sort u_12} {s : ι → Set α} : Disjoint t (⋃ i, s i) ↔ ∀ (i : ι), Disjoint t (s i)
• Set.disjoint_sUnion_left 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {S : Set (Set α)} {t : Set α} : Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t
• Set.disjoint_sUnion_right 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {s : Set α} {S : Set (Set α)} : Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t
• Set.disjoint_iUnion₂_left 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α} : Disjoint (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Disjoint (s i j) t
• Set.disjoint_iUnion₂_right 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α} : Disjoint s (⋃ i, ⋃ j, t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j)
• Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ 📋 Mathlib.Data.Set.Lattice
  {α : Type u_1} {ι : Type u_12} {Es : ι → Set α} (Es_union : ⋃ i, Es i = Set.univ) (Es_disj : Pairwise fun i j => Disjoint (Es i) (Es j)) (I : Set ι) : (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i
• Set.coe_unionEqSigmaOfDisjoint_symm_apply 📋 Mathlib.Data.Set.Lattice
  {α : Type u_12} {β : Type u_13} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : (i : α) × ↑(t i)) : ↑((Set.unionEqSigmaOfDisjoint h).symm x) = ↑x.snd
• Set.coe_snd_unionEqSigmaOfDisjoint 📋 Mathlib.Data.Set.Lattice
  {α : Type u_12} {β : Type u_13} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : ↑(⋃ i, t i)) : ↑((Set.unionEqSigmaOfDisjoint h) x).snd = ↑x
• pairwise_disjoint_fiber 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} (f : ι → α) : Pairwise (Function.onFun Disjoint fun a => f ⁻¹' {a})
• subsingleton_setOf_mem_iff_pairwise_disjoint 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {f : ι → Set α} : (∀ (a : α), {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Function.onFun Disjoint f)
• exists_ne_mem_inter_of_not_pairwise_disjoint 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {f : ι → Set α} (h : ¬Pairwise (Function.onFun Disjoint f)) : ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j
• exists_lt_mem_inter_of_not_pairwise_disjoint 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} [LinearOrder ι] {f : ι → Set α} (h : ¬Pairwise (Function.onFun Disjoint f)) : ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
• Set.pairwiseDisjoint_range_iff 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_6} {β : Type u_7} {f : α → Set β} : (Set.range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x ≠ f y → Disjoint (f x) (f y)
• Function.disjoint_mulSupport_iff 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} : Disjoint s (Function.mulSupport f) ↔ Set.EqOn f 1 s
• Function.disjoint_support_iff 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} : Disjoint s (Function.support f) ↔ Set.EqOn f 0 s
• Function.mulSupport_disjoint_iff 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [One M] {f : ι → M} {s : Set ι} : Disjoint (Function.mulSupport f) s ↔ Set.EqOn f 1 s
• Function.support_disjoint_iff 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [Zero M] {f : ι → M} {s : Set ι} : Disjoint (Function.support f) s ↔ Set.EqOn f 0 s
• Pi.mulSupport_mulSingle_disjoint 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [One M] {i j : ι} {a b : M} (ha : a ≠ 1) (hb : b ≠ 1) : Disjoint (Function.mulSupport (Pi.mulSingle i a)) (Function.mulSupport (Pi.mulSingle j b)) ↔ i ≠ j
• Pi.support_single_disjoint 📋 Mathlib.Algebra.Notation.Support
  {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] {i j : ι} {a b : M} (ha : a ≠ 0) (hb : b ≠ 0) : Disjoint (Function.support (Pi.single i a)) (Function.support (Pi.single j b)) ↔ i ≠ j
• Finset.disjoint_coe 📋 Mathlib.Data.Finset.Disjoint
  {α : Type u_2} {s t : Finset α} : Disjoint ↑s ↑t ↔ Disjoint s t
• Set.disjoint_toFinset 📋 Mathlib.Data.Fintype.Sets
  {α : Type u_1} {s t : Set α} [Fintype ↑s] [Fintype ↑t] : Disjoint s.toFinset t.toFinset ↔ Disjoint s t
• Set.Finite.disjoint_toFinset 📋 Mathlib.Data.Set.Finite.Basic
  {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite} : Disjoint hs.toFinset ht.toFinset ↔ Disjoint s t
• Disjoint.one_notMem_div_set 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [Group α] {s t : Set α} : Disjoint s t → 1 ∉ s / t
• Disjoint.zero_notMem_sub_set 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [AddGroup α] {s t : Set α} : Disjoint s t → 0 ∉ s - t
• Set.one_mem_div_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [Group α] {s t : Set α} : 1 ∈ s / t ↔ ¬Disjoint s t
• Set.one_notMem_div_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [Group α] {s t : Set α} : 1 ∉ s / t ↔ Disjoint s t
• Set.zero_mem_sub_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [AddGroup α] {s t : Set α} : 0 ∈ s - t ↔ ¬Disjoint s t
• Set.zero_notMem_sub_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [AddGroup α] {s t : Set α} : 0 ∉ s - t ↔ Disjoint s t
• Set.one_mem_inv_mul_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [Group α] {s t : Set α} : 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t
• Set.one_notMem_inv_mul_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [Group α] {s t : Set α} : 1 ∉ t⁻¹ * s ↔ Disjoint s t
• Set.zero_mem_neg_add_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [AddGroup α] {s t : Set α} : 0 ∈ -t + s ↔ ¬Disjoint s t
• Set.zero_notMem_neg_add_iff 📋 Mathlib.Algebra.Group.Pointwise.Set.Basic
  {α : Type u_2} [AddGroup α] {s t : Set α} : 0 ∉ -t + s ↔ Disjoint s t
• Set.biUnion_iInter_of_pairwise_disjoint 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {ι : Type u_9} {κ : Type u_10} [hκ : Nonempty κ] {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) (s : κ → Set ι) : ⋃ i ∈ ⋂ j, s j, f i = ⋂ j, ⋃ i ∈ s j, f i
• Set.biUnion_inter_of_pairwise_disjoint 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {ι : Type u_9} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) (s t : Set ι) : ⋃ i ∈ s ∩ t, f i = (⋃ i ∈ s, f i) ∩ ⋃ i ∈ t, f i
• Set.pairwise_disjoint_smul_iff 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s : Set β} : Pairwise (Function.onFun Disjoint fun a => a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
• Set.pairwise_disjoint_vadd_iff 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s : Set β} : Pairwise (Function.onFun Disjoint fun a => a +ᵥ s) ↔ ∀ (a : α), ((a +ᵥ s) ∩ s).Nonempty → a = 0
• Set.disjoint_smul_set 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint (a • s) (a • t) ↔ Disjoint s t
• Set.disjoint_vadd_set 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint (a +ᵥ s) (a +ᵥ t) ↔ Disjoint s t
• Set.disjoint_smul_set_left 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint (a • s) t ↔ Disjoint s (a⁻¹ • t)
• Set.disjoint_smul_set_right 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [Group α] [MulAction α β] {s t : Set β} {a : α} : Disjoint s (a • t) ↔ Disjoint (a⁻¹ • s) t
• Set.disjoint_vadd_set_left 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint (a +ᵥ s) t ↔ Disjoint s (-a +ᵥ t)
• Set.disjoint_vadd_set_right 📋 Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
  {α : Type u_2} {β : Type u_3} [AddGroup α] [AddAction α β] {s t : Set β} {a : α} : Disjoint s (a +ᵥ t) ↔ Disjoint (-a +ᵥ s) t
• Function.Embedding.sumSet 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) : ↑s ⊕ ↑t ↪ α
• Function.Embedding.sigmaSet 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) : (i : ι) × ↑(s i) ↪ α
• Function.Embedding.sumSet_range 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) : Set.range ⇑(Function.Embedding.sumSet h) = s ∪ t
• Function.Embedding.sigmaSet_range 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) : Set.range ⇑(Function.Embedding.sigmaSet h) = ⋃ i, s i
• Function.Embedding.coe_sumSet 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) : ⇑(Function.Embedding.sumSet h) = Sum.elim Subtype.val Subtype.val
• Function.Embedding.sumSet_apply 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) (a✝ : ↑s ⊕ ↑t) : (Function.Embedding.sumSet h) a✝ = Sum.elim Subtype.val Subtype.val a✝
• Function.Embedding.sigmaSet_apply 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) (x : (i : ι) × ↑(s i)) : (Function.Embedding.sigmaSet h) x = ↑x.snd
• Function.Embedding.coe_sigmaSet 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) : ⇑(Function.Embedding.sigmaSet h) = fun x => ↑x.snd
• Function.Embedding.sumSet_preimage_inl 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t r : Set α} (h : Disjoint s t) : Subtype.val '' (Sum.inl ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' r)) = r ∩ s
• Function.Embedding.sumSet_preimage_inr 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {s t r : Set α} (h : Disjoint s t) : Subtype.val '' (Sum.inr ⁻¹' (⇑(Function.Embedding.sumSet h) ⁻¹' r)) = r ∩ t
• Function.Embedding.sigmaSet_preimage 📋 Mathlib.Logic.Embedding.Set
  {α : Type u_1} {ι : Type u_2} {s : ι → Set α} (h : Pairwise (Function.onFun Disjoint s)) (i : ι) (r : Set α) : Subtype.val '' (Sigma.mk i ⁻¹' (⇑(Function.Embedding.sigmaSet h) ⁻¹' r)) = r ∩ s i
• Pairwise.biUnion_injective 📋 Mathlib.Data.Set.Pairwise.Lattice
  {α : Type u_1} {ι : Type u_2} {f : ι → Set α} (h₀ : Pairwise (Function.onFun Disjoint f)) (h₁ : ∀ (i : ι), (f i).Nonempty) : Function.Injective fun s => ⋃ i ∈ s, f i
• Pairwise.subset_of_biUnion_subset_biUnion 📋 Mathlib.Data.Set.Pairwise.Lattice
  {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s t : Set ι} (h₀ : Pairwise (Function.onFun Disjoint f)) (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t
• Set.finite_iUnion_iff 📋 Mathlib.Data.Set.Finite.Lattice
  {α : Type u} {ι : Type u_1} {s : ι → Set α} (hs : Pairwise fun i j => Disjoint (s i) (s j)) : (⋃ i, s i).Finite ↔ (∀ (i : ι), (s i).Finite) ∧ {i | (s i).Nonempty}.Finite
• AddAction.disjoint_image_image_iff 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {U V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V
• MulAction.disjoint_image_image_iff 📋 Mathlib.GroupTheory.GroupAction.Defs
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {U V : Set α} : Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g • x ∉ V
• Set.countable_setOf_nonempty_of_disjoint 📋 Mathlib.Data.Set.Countable
  {α : Type u} {β : Type v} {f : β → Set α} (hf : Pairwise (Function.onFun Disjoint f)) {s : Set α} (h'f : ∀ (t : β), f t ⊆ s) (hs : s.Countable) : {t | (f t).Nonempty}.Countable
• Cardinal.mk_iUnion_eq_sum_mk 📋 Mathlib.SetTheory.Cardinal.Basic
  {α ι : Type u} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) : Cardinal.mk ↑(⋃ i, f i) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
• Cardinal.mk_iUnion_eq_sum_mk_lift 📋 Mathlib.SetTheory.Cardinal.Basic
  {α : Type u} {ι : Type v} {f : ι → Set α} (h : Pairwise (Function.onFun Disjoint f)) : Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) = Cardinal.sum fun i => Cardinal.mk ↑(f i)
• Cardinal.mk_union_of_disjoint 📋 Mathlib.SetTheory.Cardinal.Basic
  {α : Type u} {S T : Set α} (H : Disjoint S T) : Cardinal.mk ↑(S ∪ T) = Cardinal.mk ↑S + Cardinal.mk ↑T
• Disjoint.of_span₀ 📋 Mathlib.LinearAlgebra.Span.Defs
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set M} (hst : Disjoint (Submodule.span R s) (Submodule.span R t)) (h0s : 0 ∉ s) : Disjoint s t
• Disjoint.of_span 📋 Mathlib.LinearAlgebra.Span.Defs
  {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set M} (hst : Disjoint (Submodule.span R s) (Submodule.span R t)) : Disjoint (s \ {0}) t
• Set.indicator_eq_zero 📋 Mathlib.Algebra.Notation.Indicator
  {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : (s.indicator f = fun x => 0) ↔ Disjoint (Function.support f) s
• Set.mulIndicator_eq_one 📋 Mathlib.Algebra.Notation.Indicator
  {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} : (s.mulIndicator f = fun x => 1) ↔ Disjoint (Function.mulSupport f) s
• Set.indicator_eq_zero' 📋 Mathlib.Algebra.Notation.Indicator
  {α : Type u_1} {M : Type u_3} [Zero M] {s : Set α} {f : α → M} : s.indicator f = 0 ↔ Disjoint (Function.support f) s
• Set.mulIndicator_eq_one' 📋 Mathlib.Algebra.Notation.Indicator
  {α : Type u_1} {M : Type u_3} [One M] {s : Set α} {f : α → M} : s.mulIndicator f = 1 ↔ Disjoint (Function.mulSupport f) s
• Set.indicator_union_of_disjoint 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [AddZeroClass M] {s t : Set α} (h : Disjoint s t) (f : α → M) : (s ∪ t).indicator f = fun a => s.indicator f a + t.indicator f a
• Set.mulIndicator_union_of_disjoint 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [MulOneClass M] {s t : Set α} (h : Disjoint s t) (f : α → M) : (s ∪ t).mulIndicator f = fun a => s.mulIndicator f a * t.mulIndicator f a
• Set.indicator_add_eq_left 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [AddZeroClass M] {f g : α → M} (h : Disjoint (Function.support f) (Function.support g)) : (Function.support f).indicator (f + g) = f
• Set.indicator_add_eq_right 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [AddZeroClass M] {f g : α → M} (h : Disjoint (Function.support f) (Function.support g)) : (Function.support g).indicator (f + g) = g
• Set.mulIndicator_mul_eq_left 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [MulOneClass M] {f g : α → M} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) : (Function.mulSupport f).mulIndicator (f * g) = f
• Set.mulIndicator_mul_eq_right 📋 Mathlib.Algebra.Group.Indicator
  {α : Type u_1} {M : Type u_3} [MulOneClass M] {f g : α → M} (h : Disjoint (Function.mulSupport f) (Function.mulSupport g)) : (Function.mulSupport g).mulIndicator (f * g) = g
• finprod_mem_iUnion 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {ι : Type u_3} {M : Type u_5} [CommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α} (h : Pairwise (Function.onFun Disjoint t)) (ht : ∀ (i : ι), (t i).Finite) : ∏ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∏ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
• finsum_mem_iUnion 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {ι : Type u_3} {M : Type u_5} [AddCommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α} (h : Pairwise (Function.onFun Disjoint t)) (ht : ∀ (i : ι), (t i).Finite) : ∑ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∑ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
• finprod_mem_union 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint s t) (hs : s.Finite) (ht : t.Finite) : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
• finsum_mem_union 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint s t) (hs : s.Finite) (ht : t.Finite) : ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
• finprod_mem_union' 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint s t) (hs : (s ∩ Function.mulSupport f).Finite) (ht : (t ∩ Function.mulSupport f).Finite) : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
• finsum_mem_union' 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint s t) (hs : (s ∩ Function.support f).Finite) (ht : (t ∩ Function.support f).Finite) : ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
• finprod_mem_union'' 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [CommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint (s ∩ Function.mulSupport f) (t ∩ Function.mulSupport f)) (hs : (s ∩ Function.mulSupport f).Finite) (ht : (t ∩ Function.mulSupport f).Finite) : ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
• finsum_mem_union'' 📋 Mathlib.Algebra.BigOperators.Finprod
  {α : Type u_1} {M : Type u_5} [AddCommMonoid M] {f : α → M} {s t : Set α} (hst : Disjoint (s ∩ Function.support f) (t ∩ Function.support f)) (hs : (s ∩ Function.support f).Finite) (ht : (t ∩ Function.support f).Finite) : ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
• Finsupp.disjoint_supported_supported 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {s t : Set α} (h : Disjoint s t) : Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t)
• Finsupp.disjoint_supported_supported_iff 📋 Mathlib.LinearAlgebra.Finsupp.Supported
  {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] {s t : Set α} : Disjoint (Finsupp.supported M R s) (Finsupp.supported M R t) ↔ Disjoint s t
• LinearIndependent.disjoint_span_image 📋 Mathlib.LinearAlgebra.LinearIndependent.Basic
  {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [Semiring R] [AddCommMonoid M] [Module R M] (hv : LinearIndependent R v) {s t : Set ι} (hs : Disjoint s t) : Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
• linearIndepOn_id_union_iff 📋 Mathlib.LinearAlgebra.LinearIndependent.Basic
  {R : Type u_2} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s t : Set M} (hdj : Disjoint s t) : LinearIndepOn R id (s ∪ t) ↔ LinearIndepOn R id s ∧ LinearIndepOn R id t ∧ Disjoint (Submodule.span R s) (Submodule.span R t)
• linearIndepOn_union_iff 📋 Mathlib.LinearAlgebra.LinearIndependent.Basic
  {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [Ring R] [AddCommGroup M] [Module R M] {t : Set ι} (hdj : Disjoint s t) : LinearIndepOn R v (s ∪ t) ↔ LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
• Set.encard_union_eq 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) : (s ∪ t).encard = s.encard + t.encard
• Set.ncard_union_eq 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s t : Set α} (h : Disjoint s t) (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard = s.ncard + t.ncard
• Set.ncard_union_eq_iff 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s t : Set α} (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) : (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t
• Set.ncard_union_lt 📋 Mathlib.Data.Set.Card
  {α : Type u_1} {s t : Set α} (hs : s.Finite := by toFinite_tac) (ht : t.Finite := by toFinite_tac) (h : ¬Disjoint s t) : (s ∪ t).ncard < s.ncard + t.ncard
• LinearMap.iSup_range_single_eq_iInf_ker_proj 📋 Mathlib.LinearAlgebra.Pi
  (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] {I J : Set ι} (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) (hI : I.Finite) : ⨆ i ∈ I, (LinearMap.single R φ i).range = ⨅ i ∈ J, (LinearMap.proj i).ker
• LinearMap.iSup_range_single_le_iInf_ker_proj 📋 Mathlib.LinearAlgebra.Pi
  (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I J : Set ι) (h : Disjoint I J) : ⨆ i ∈ I, (LinearMap.single R φ i).range ≤ ⨅ i ∈ J, (LinearMap.proj i).ker
• LinearMap.disjoint_single_single 📋 Mathlib.LinearAlgebra.Pi
  (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] [DecidableEq ι] (I J : Set ι) (h : Disjoint I J) : Disjoint (⨆ i ∈ I, (LinearMap.single R φ i).range) (⨆ i ∈ J, (LinearMap.single R φ i).range)
• LinearMap.iInfKerProjEquiv 📋 Mathlib.LinearAlgebra.Pi
  (R : Type u) {ι : Type x} [Semiring R] (φ : ι → Type i) [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] {I J : Set ι} [DecidablePred fun i => i ∈ I] (hd : Disjoint I J) (hu : Set.univ ⊆ I ∪ J) : ↥(⨅ i ∈ J, (LinearMap.proj i).ker) ≃ₗ[R] (i : ↑I) → φ ↑i
• Ideal.exists_disjoint_powers_of_span_eq_top 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (s : Set α) (hs : Ideal.span s = ⊤) (I : Ideal α) (hI : I ≠ ⊤) : ∃ r ∈ s, Disjoint ↑I ↑(Submonoid.powers r)
• Ideal.isPrime_of_maximally_disjoint 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) (maximally_disjoint : ∀ (J : Ideal α), I < J → ¬Disjoint ↑J ↑S) : I.IsPrime
• Ideal.exists_le_prime_disjoint 📋 Mathlib.RingTheory.Ideal.Maximal
  {α : Type u} [CommSemiring α] (I : Ideal α) (S : Submonoid α) (disjoint : Disjoint ↑I ↑S) : ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S
• Filter.NeBot.not_disjoint 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f : Filter α} {s t : Set α} (hf : f.NeBot) (hs : s ∈ f) (ht : t ∈ f) : ¬Disjoint s t
• Filter.disjoint_of_disjoint_of_mem 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f g : Filter α} {s t : Set α} (h : Disjoint s t) (hs : s ∈ f) (ht : t ∈ g) : Disjoint f g
• Filter.disjoint_iff 📋 Mathlib.Order.Filter.Basic
  {α : Type u} {f g : Filter α} : Disjoint f g ↔ ∃ s ∈ f, ∃ t ∈ g, Disjoint s t
• Disjoint.filter_principal 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {s t : Set α} : Disjoint s t → Disjoint (Filter.principal s) (Filter.principal t)
• Filter.disjoint_principal_principal 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {s t : Set α} : Disjoint (Filter.principal s) (Filter.principal t) ↔ Disjoint s t
• Disjoint.exists_mem_filter_basis 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (h : Disjoint l l') (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
• Filter.HasBasis.disjoint_iff 📋 Mathlib.Order.Filter.Bases.Basic
  {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') : Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
• Set.Iio_disjoint_Ioi_same 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a : α} : Disjoint (Set.Iio a) (Set.Ioi a)
• Set.Ioi_disjoint_Iio_same 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a : α} : Disjoint (Set.Ioi a) (Set.Iio a)
• Set.Ioc_disjoint_Ioi_same 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a b : α} : Disjoint (Set.Ioc a b) (Set.Ioi b)
• Set.Ico_disjoint_Ico_same 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a b c : α} : Disjoint (Set.Ico a b) (Set.Ico b c)
• Set.Iic_disjoint_Ioi 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Set.Iic a) (Set.Ioi b)
• Set.Iio_disjoint_Ici 📋 Mathlib.Order.Interval.Set.Disjoint
  {α : Type v} [Preorder α] {a b : α} (h : a ≤ b) : Disjoint (Set.Iio a) (Set.Ici b)

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.

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

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

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

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 128218b serving mathlib revision d8f2208