Loogle!

Result

Found 363 declarations mentioning Function.onFun. Of these, only the first 200 are shown.

• Function.onFun 📋 Mathlib.Logic.Function.Defs
  {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) : α → α → φ
• Function.onFun_apply 📋 Mathlib.Logic.Function.Basic
  {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : β → β → γ) (g : α → β) (a b : α) : Function.onFun f g a b = f (g a) (g b)
• Equivalence.comap 📋 Mathlib.Logic.Relation
  {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : Equivalence r) (f : α → β) : Equivalence (Function.onFun r f)
• Reflexive.comap 📋 Mathlib.Logic.Relation
  {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : Reflexive r) (f : α → β) : Reflexive (Function.onFun r f)
• Symmetric.comap 📋 Mathlib.Logic.Relation
  {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : Symmetric r) (f : α → β) : Symmetric (Function.onFun r f)
• Transitive.comap 📋 Mathlib.Logic.Relation
  {α : Type u_1} {β : Type u_2} {r : β → β → Prop} (h : Transitive r) (f : α → β) : Transitive (Function.onFun r f)
• WellFounded.onFun 📋 Mathlib.Order.WellFounded
  {α : Sort u_4} {β : Sort u_5} {r : β → β → Prop} {f : α → β} : WellFounded r → WellFounded (Function.onFun r f)
• Function.Injective.pairwise_ne 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {ι : Type u_3} {f : ι → α} : Function.Injective f → Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) f)
• Function.injective_iff_pairwise_ne 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {ι : Type u_3} {f : ι → α} : Function.Injective f ↔ Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) f)
• Pairwise.comp_of_injective 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (hr : Pairwise r) {f : β → α} (hf : Function.Injective f) : Pairwise (Function.onFun r f)
• Pairwise.of_comp_of_surjective 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} (hr : Pairwise (Function.onFun r f)) (hf : Function.Surjective f) : Pairwise r
• Function.Bijective.pairwise_comp_iff 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : β → α} (hf : Function.Bijective f) : Pairwise (Function.onFun r f) ↔ Pairwise r
• Set.Pairwise.on_injective 📋 Mathlib.Logic.Pairwise
  {α : Type u_1} {ι : Type u_3} {r : α → α → Prop} {f : ι → α} {s : Set α} (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ (x : ι), f x ∈ s) : Pairwise (Function.onFun r f)
• 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)
• Pairwise.range_pairwise 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} (hr : Pairwise (Function.onFun r f)) : (Set.range f).Pairwise r
• pairwise_on_bool 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {r : α → α → Prop} (hr : Symmetric r) {a b : α} : Pairwise (Function.onFun r fun c => bif c then a else b) ↔ r a b
• Set.Pairwise.image 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : Set ι} (h : s.Pairwise (Function.onFun r f)) : (f '' s).Pairwise r
• Set.InjOn.pairwise_image 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : Set ι} (h : Set.InjOn f s) : (f '' s).Pairwise r ↔ s.Pairwise (Function.onFun r f)
• Pairwise.pairwiseDisjoint 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {f : ι → α} (h : Pairwise (Function.onFun Disjoint f)) (s : Set ι) : s.PairwiseDisjoint f
• pairwise_disjoint_on_bool 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} : Pairwise (Function.onFun Disjoint fun c => bif c then a else b) ↔ Disjoint a b
• Set.PairwiseDisjoint.eq_1 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] (s : Set ι) (f : ι → α) : s.PairwiseDisjoint f = s.Pairwise (Function.onFun Disjoint f)
• Set.pairwise_iff_exists_forall 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop} [IsEquiv ι r] : s.Pairwise (Function.onFun r f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
• Set.Nonempty.pairwise_iff_exists_forall 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} [IsEquiv α r] {s : Set ι} (hs : s.Nonempty) : s.Pairwise (Function.onFun r f) ↔ ∃ z, ∀ x ∈ s, r (f x) z
• Symmetric.pairwise_on 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} [LinearOrder ι] (hr : Symmetric r) (f : ι → α) : Pairwise (Function.onFun r f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)
• pairwise_disjoint_mono 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} {f g : ι → α} [PartialOrder α] [OrderBot α] (hs : Pairwise (Function.onFun Disjoint f)) (h : g ≤ f) : Pairwise (Function.onFun Disjoint g)
• pairwise_disjoint_on 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] [LinearOrder ι] (f : ι → α) : Pairwise (Function.onFun Disjoint f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)
• 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)
• Pairwise.disjoint_extend_bot 📋 Mathlib.Data.Set.Pairwise.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder γ] [OrderBot γ] {e : α → β} {f : α → γ} (hf : Pairwise (Function.onFun Disjoint f)) (he : Function.FactorsThrough f e) : Pairwise (Function.onFun Disjoint (Function.extend e 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.pairwise_disjoint_Ico_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun n => Set.Ico (↑n) (↑n + 1))
• Set.pairwise_disjoint_Ico_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ico (b ^ n) (b ^ (n + 1)))
• Set.pairwise_disjoint_Ico_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ico (n • b) ((n + 1) • b))
• Set.pairwise_disjoint_Ioc_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (↑n) (↑n + 1))
• Set.pairwise_disjoint_Ioc_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (b ^ n) (b ^ (n + 1)))
• Set.pairwise_disjoint_Ioc_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (n • b) ((n + 1) • b))
• Set.pairwise_disjoint_Ioo_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  (α : Type u_1) [Ring α] [PartialOrder α] [IsOrderedRing α] : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (↑n) (↑n + 1))
• Set.pairwise_disjoint_Ioo_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (b ^ n) (b ^ (n + 1)))
• Set.pairwise_disjoint_Ioo_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (n • b) ((n + 1) • b))
• Set.pairwise_disjoint_Ico_add_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ico (a + ↑n) (a + ↑n + 1))
• Set.pairwise_disjoint_Ico_add_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ico (a + n • b) (a + (n + 1) • b))
• Set.pairwise_disjoint_Ico_mul_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ico (a * b ^ n) (a * b ^ (n + 1)))
• Set.pairwise_disjoint_Ioc_add_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a + ↑n) (a + ↑n + 1))
• Set.pairwise_disjoint_Ioc_add_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a + n • b) (a + (n + 1) • b))
• Set.pairwise_disjoint_Ioc_mul_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioc (a * b ^ n) (a * b ^ (n + 1)))
• Set.pairwise_disjoint_Ioo_add_intCast 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [Ring α] [PartialOrder α] [IsOrderedRing α] (a : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a + ↑n) (a + ↑n + 1))
• Set.pairwise_disjoint_Ioo_add_zsmul 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a + n • b) (a + (n + 1) • b))
• Set.pairwise_disjoint_Ioo_mul_zpow 📋 Mathlib.Algebra.Order.Interval.Set.Group
  {α : Type u_1} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a b : α) : Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a * b ^ n) (a * b ^ (n + 1)))
• List.nodup_bind 📋 Mathlib.Data.List.Nodup
  {α : Type u} {β : Type v} {l₁ : List α} {f : α → List β} : (List.flatMap f l₁).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ List.Pairwise (Function.onFun List.Disjoint f) l₁
• List.nodup_flatMap 📋 Mathlib.Data.List.Nodup
  {α : Type u} {β : Type v} {l₁ : List α} {f : α → List β} : (List.flatMap f l₁).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ List.Pairwise (Function.onFun List.Disjoint f) l₁
• Finset.pairwise_subtype_iff_pairwise_finset 📋 Mathlib.Data.Finset.Defs
  {α : Type u_1} {s : Finset α} (r : α → α → Prop) : Pairwise (Function.onFun r fun x => ↑x) ↔ (↑s).Pairwise r
• Finset.pairwise_subtype_iff_pairwise_finset' 📋 Mathlib.Data.Finset.Defs
  {α : Type u_1} {β : Type u_2} {s : Finset α} (r : β → β → Prop) (f : α → β) : Pairwise (Function.onFun r fun x => f ↑x) ↔ (↑s).Pairwise (Function.onFun r f)
• Finset.pairwise_cons 📋 Mathlib.Data.Finset.Insert
  {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (r : α → α → Prop) : Pairwise (Function.onFun r fun a_1 => ↑a_1) ↔ Pairwise (Function.onFun r fun a => ↑a) ∧ ∀ b ∈ s, r a b ∧ r b a
• Finset.pairwise_cons' 📋 Mathlib.Data.Finset.Insert
  {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) : Pairwise (Function.onFun r fun a_1 => f ↑a_1) ↔ Pairwise (Function.onFun r fun a => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
• Multiset.nodup_bind 📋 Mathlib.Data.Multiset.Bind
  {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → Multiset β} : (s.bind f).Nodup ↔ (∀ a ∈ s, (f a).Nodup) ∧ Multiset.Pairwise (Function.onFun Disjoint f) s
• Finset.disjiUnion_map 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h : (↑s).PairwiseDisjoint t} : Finset.map f (s.disjiUnion t h) = s.disjiUnion (fun a => Finset.map f (t a)) ⋯
• Function.onFun.eq_1 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) (x y : α) : Function.onFun f g x y = f (g x) (g y)
• exists_seq_of_forall_finset_exists' 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_4} (P : α → Prop) (r : α → α → Prop) [IsSymm α r] (h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y) : ∃ f, (∀ (n : ℕ), P (f n)) ∧ Pairwise (Function.onFun r f)
• Finset.noncommProd 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) : β
• Finset.noncommSum 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) : β
• Finset.noncommProd_empty 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (f : α → β) (h : (↑∅).Pairwise (Function.onFun Commute f)) : ∅.noncommProd f h = 1
• Finset.noncommSum_empty 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (f : α → β) (h : (↑∅).Pairwise (Function.onFun AddCommute f)) : ∅.noncommSum f h = 0
• Finset.noncommProd_lemma 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) : {x | x ∈ Multiset.map f s.val}.Pairwise Commute
• Finset.noncommSum_lemma 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) : {x | x ∈ Multiset.map f s.val}.Pairwise AddCommute
• Finset.noncommProd.eq_1 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) : s.noncommProd f comm = (Multiset.map f s.val).noncommProd ⋯
• Finset.noncommSum.eq_1 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) : s.noncommSum f comm = (Multiset.map f s.val).noncommSum ⋯
• Finset.noncommProd_commute 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (y : β) (h : ∀ x ∈ s, Commute y (f x)) : Commute y (s.noncommProd f comm)
• Finset.noncommSum_addCommute 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (y : β) (h : ∀ x ∈ s, AddCommute y (f x)) : AddCommute y (s.noncommSum f comm)
• Finset.noncommProd_toFinset 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (l : List α) (f : α → β) (comm : (↑l.toFinset).Pairwise (Function.onFun Commute f)) (hl : l.Nodup) : l.toFinset.noncommProd f comm = (List.map f l).prod
• Finset.noncommSum_toFinset 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (l : List α) (f : α → β) (comm : (↑l.toFinset).Pairwise (Function.onFun AddCommute f)) (hl : l.Nodup) : l.toFinset.noncommSum f comm = (List.map f l).sum
• Finset.noncommProd_eq_pow_card 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (m : β) (h : ∀ x ∈ s, f x = m) : s.noncommProd f comm = m ^ s.card
• Finset.noncommSum_eq_card_nsmul 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (m : β) (h : ∀ x ∈ s, f x = m) : s.noncommSum f comm = s.card • m
• Finset.noncommProd_induction 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (p : β → Prop) (hom : ∀ (a b : β), p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) : p (s.noncommProd f comm)
• Finset.noncommSum_induction 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (p : β → Prop) (hom : ∀ (a b : β), p a → p b → p (a + b)) (unit : p 0) (base : ∀ x ∈ s, p (f x)) : p (s.noncommSum f comm)
• Finset.noncommProd_mul_distrib_aux 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] {s : Finset α} {f g : α → β} (comm_ff : (↑s).Pairwise (Function.onFun Commute f)) (comm_gg : (↑s).Pairwise (Function.onFun Commute g)) (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)) : (↑s).Pairwise fun x y => Commute ((f * g) x) ((f * g) y)
• Finset.noncommSum_add_distrib_aux 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] {s : Finset α} {f g : α → β} (comm_ff : (↑s).Pairwise (Function.onFun AddCommute f)) (comm_gg : (↑s).Pairwise (Function.onFun AddCommute g)) (comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)) : (↑s).Pairwise fun x y => AddCommute ((f + g) x) ((f + g) y)
• Finset.noncommProd_insert_of_not_mem 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm : (↑(insert a s)).Pairwise (Function.onFun Commute f)) (ha : a ∉ s) : (insert a s).noncommProd f comm = f a * s.noncommProd f ⋯
• Finset.noncommProd_insert_of_not_mem' 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm : (↑(insert a s)).Pairwise (Function.onFun Commute f)) (ha : a ∉ s) : (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a
• Finset.noncommSum_insert_of_not_mem 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm : (↑(insert a s)).Pairwise (Function.onFun AddCommute f)) (ha : a ∉ s) : (insert a s).noncommSum f comm = f a + s.noncommSum f ⋯
• Finset.noncommSum_insert_of_not_mem' 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm : (↑(insert a s)).Pairwise (Function.onFun AddCommute f)) (ha : a ∉ s) : (insert a s).noncommSum f comm = s.noncommSum f ⋯ + f a
• Finset.noncommProd_mul_distrib 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] {s : Finset α} (f g : α → β) (comm_ff : (↑s).Pairwise (Function.onFun Commute f)) (comm_gg : (↑s).Pairwise (Function.onFun Commute g)) (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)) : s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
• Finset.noncommSum_add_distrib 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] {s : Finset α} (f g : α → β) (comm_ff : (↑s).Pairwise (Function.onFun AddCommute f)) (comm_gg : (↑s).Pairwise (Function.onFun AddCommute g)) (comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)) : s.noncommSum (f + g) ⋯ = s.noncommSum f comm_ff + s.noncommSum g comm_gg
• Finset.map_noncommProd 📋 Mathlib.Data.Finset.NoncommProd
  {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Monoid β] [Monoid γ] [FunLike F β γ] [MonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (g : F) : g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) ⋯
• Finset.map_noncommSum 📋 Mathlib.Data.Finset.NoncommProd
  {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddMonoid β] [AddMonoid γ] [FunLike F β γ] [AddMonoidHomClass F β γ] (s : Finset α) (f : α → β) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (g : F) : g (s.noncommSum f comm) = s.noncommSum (fun i => g (f i)) ⋯
• Finset.mul_noncommProd_erase 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → Function.onFun Commute f x x_1 := ⋯) : f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm
• Finset.noncommProd_erase_mul 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] (s : Finset α) {a : α} (h : a ∈ s) (f : α → β) (comm : (↑s).Pairwise (Function.onFun Commute f)) (comm' : ∀ x ∈ ↑(s.erase a), ∀ x_1 ∈ ↑(s.erase a), x ≠ x_1 → Function.onFun Commute f x x_1 := ⋯) : (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm
• Finset.noncommProd_singleton 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (a : α) (f : α → β) : {a}.noncommProd f ⋯ = f a
• Finset.noncommSum_singleton 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (a : α) (f : α → β) : {a}.noncommSum f ⋯ = f a
• Finset.noncommProd_cons 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun Commute f)) : (Finset.cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
• Finset.noncommProd_cons' 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun Commute f)) : (Finset.cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
• Finset.noncommSum_cons 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun AddCommute f)) : (Finset.cons a s ha).noncommSum f comm = f a + s.noncommSum f ⋯
• Finset.noncommSum_cons' 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] (s : Finset α) (a : α) (f : α → β) (ha : a ∉ s) (comm : (↑(Finset.cons a s ha)).Pairwise (Function.onFun AddCommute f)) : (Finset.cons a s ha).noncommSum f comm = s.noncommSum f ⋯ + f a
• Finset.noncommProd_union_of_disjoint 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (f : α → β) (comm : {x | x ∈ s ∪ t}.Pairwise (Function.onFun Commute f)) : (s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯
• Finset.noncommSum_union_of_disjoint 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] [DecidableEq α] {s t : Finset α} (h : Disjoint s t) (f : α → β) (comm : {x | x ∈ s ∪ t}.Pairwise (Function.onFun AddCommute f)) : (s ∪ t).noncommSum f comm = s.noncommSum f ⋯ + t.noncommSum f ⋯
• Finset.noncommProd_congr 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [Monoid β] {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) (comm : (↑s₁).Pairwise (Function.onFun Commute f)) : s₁.noncommProd f comm = s₂.noncommProd g ⋯
• Finset.noncommSum_congr 📋 Mathlib.Data.Finset.NoncommProd
  {α : Type u_3} {β : Type u_4} [AddMonoid β] {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) (comm : (↑s₁).Pairwise (Function.onFun AddCommute f)) : s₁.noncommSum f comm = s₂.noncommSum g ⋯
• AddSubmonoid.noncommSum_mem 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
  {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : (↑t).Pairwise (Function.onFun AddCommute f)) (h : ∀ c ∈ t, f c ∈ S) : t.noncommSum f comm ∈ S
• Submonoid.noncommProd_mem 📋 Mathlib.Algebra.Group.Submonoid.BigOperators
  {M : Type u_1} [Monoid M] (S : Submonoid M) {ι : Type u_4} (t : Finset ι) (f : ι → M) (comm : (↑t).Pairwise (Function.onFun Commute f)) (h : ∀ c ∈ t, f c ∈ S) : t.noncommProd f comm ∈ S
• Set.disjoint_accumulate 📋 Mathlib.Data.Set.Accumulate
  {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] (hs : Pairwise (Function.onFun Disjoint s)) {i j : α} (hij : i < j) : Disjoint (Set.Accumulate s i) (s j)
• List.pairwise_sublists 📋 Mathlib.Data.List.Sublists
  {α : Type u} {R : α → α → Prop} {l : List α} (H : List.Pairwise R l) : List.Pairwise (Function.onFun (List.Lex R) List.reverse) l.sublists
• 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
• 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.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.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.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
• List.pairwise_disjoint_of_coe_toFinset_pairwiseDisjoint 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_5} {ι : Type u_6} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hl : (↑l.toFinset).PairwiseDisjoint f) (hn : l.Nodup) : List.Pairwise (Function.onFun Disjoint f) l
• List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint 📋 Mathlib.Data.Finset.Pairwise
  {α : Type u_5} {ι : Type u_6} [PartialOrder α] [OrderBot α] [DecidableEq ι] {l : List ι} {f : ι → α} (hn : l.Nodup) : (↑l.toFinset).PairwiseDisjoint f ↔ List.Pairwise (Function.onFun Disjoint f) l
• iSupIndep_iff_pairwiseDisjoint 📋 Mathlib.Order.SupIndep
  {α : Type u_1} {ι : Type u_3} [Order.Frame α] {f : ι → α} : iSupIndep f ↔ Pairwise (Function.onFun Disjoint f)
• independent_iff_pairwiseDisjoint 📋 Mathlib.Order.SupIndep
  {α : Type u_1} {ι : Type u_3} [Order.Frame α] {f : ι → α} : iSupIndep f ↔ Pairwise (Function.onFun Disjoint f)
• iSupIndep.pairwiseDisjoint 📋 Mathlib.Order.SupIndep
  {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) : Pairwise (Function.onFun Disjoint t)
• CompleteLattice.Independent.pairwiseDisjoint 📋 Mathlib.Order.SupIndep
  {α : Type u_1} {ι : Type u_3} [CompleteLattice α] {t : ι → α} (ht : iSupIndep t) : Pairwise (Function.onFun Disjoint t)
• Set.wellFoundedOn_range 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} : (Set.range f).WellFoundedOn r ↔ WellFounded (Function.onFun r f)
• Set.wellFoundedOn_image 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} {s : Set β} : (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (Function.onFun r f)
• Set.WellFoundedOn.mapsTo 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_6} {β : Type u_7} {r : α → α → Prop} (f : β → α) {s : Set α} {t : Set β} (h : Set.MapsTo f t s) (hw : s.WellFoundedOn r) : t.WellFoundedOn (Function.onFun r f)
• WellFounded.prod_lex_of_wellFoundedOn_fiber 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β} (hα : WellFounded (Function.onFun rα f)) (hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) : WellFounded (Function.onFun (Prod.Lex rα rβ) fun c => (f c, g c))
• Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β} {s : Set γ} (hα : s.WellFoundedOn (Function.onFun rα f)) (hβ : ∀ (a : α), (s ∩ f ⁻¹' {a}).WellFoundedOn (Function.onFun rβ g)) : s.WellFoundedOn (Function.onFun (Prod.Lex rα rβ) fun c => (f c, g c))
• WellFounded.sigma_lex_of_wellFoundedOn_fiber 📋 Mathlib.Order.WellFoundedSet
  {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι} {g : (i : ι) → γ → π i} (hι : WellFounded (Function.onFun rι f)) (hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (Function.onFun (rπ i) (g i))) : WellFounded (Function.onFun (Sigma.Lex rι rπ) fun c => ⟨f c, g (f c) c⟩)
• Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber 📋 Mathlib.Order.WellFoundedSet
  {ι : Type u_1} {γ : Type u_4} {π : ι → Type u_5} {rι : ι → ι → Prop} {rπ : (i : ι) → π i → π i → Prop} {f : γ → ι} {g : (i : ι) → γ → π i} {s : Set γ} (hι : s.WellFoundedOn (Function.onFun rι f)) (hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (Function.onFun (rπ i) (g i))) : s.WellFoundedOn (Function.onFun (Sigma.Lex rι rπ) fun c => ⟨f c, g (f c) c⟩)
• 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
• Fintype.prod_dvd_of_isRelPrime 📋 Mathlib.RingTheory.Coprime.Lemmas
  {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} [Fintype I] (Hs : Pairwise (Function.onFun IsRelPrime s)) (Hs1 : ∀ (i : I), s i ∣ z) : ∏ x, s x ∣ z
• Fintype.prod_dvd_of_coprime 📋 Mathlib.RingTheory.Coprime.Lemmas
  {R : Type u} {I : Type v} [CommSemiring R] {z : R} {s : I → R} [Fintype I] (Hs : Pairwise (Function.onFun IsCoprime s)) (Hs1 : ∀ (i : I), s i ∣ z) : ∏ x, s x ∣ z
• Finset.prod_dvd_of_isRelPrime 📋 Mathlib.RingTheory.Coprime.Lemmas
  {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {z : α} {s : I → α} {t : Finset I} : (↑t).Pairwise (Function.onFun IsRelPrime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
• Finset.prod_dvd_of_coprime 📋 Mathlib.RingTheory.Coprime.Lemmas
  {R : Type u} {I : Type v} [CommSemiring R] {z : R} {s : I → R} {t : Finset I} : (↑t).Pairwise (Function.onFun IsCoprime s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z
• pairwise_coprime_iff_coprime_prod 📋 Mathlib.RingTheory.Coprime.Lemmas
  {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] : Pairwise (Function.onFun IsCoprime fun i => s ↑i) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
• exists_sum_eq_one_iff_pairwise_coprime' 📋 Mathlib.RingTheory.Coprime.Lemmas
  {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} [Fintype I] [Nonempty I] [DecidableEq I] : (∃ μ, ∑ i, μ i * ∏ j ∈ {i}ᶜ, s j = 1) ↔ Pairwise (Function.onFun IsCoprime s)
• pairwise_isRelPrime_iff_isRelPrime_prod 📋 Mathlib.RingTheory.Coprime.Lemmas
  {α : Type u_2} {I : Type u_1} [CommMonoid α] [DecompositionMonoid α] {s : I → α} {t : Finset I} [DecidableEq I] : Pairwise (Function.onFun IsRelPrime fun i => s ↑i) ↔ ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
• exists_sum_eq_one_iff_pairwise_coprime 📋 Mathlib.RingTheory.Coprime.Lemmas
  {R : Type u} {I : Type v} [CommSemiring R] {s : I → R} {t : Finset I} [DecidableEq I] (h : t.Nonempty) : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (Function.onFun IsCoprime fun i => s ↑i)
• Ideal.finset_inf_span_singleton 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R) (hI : (↑s).Pairwise (Function.onFun IsCoprime I)) : (s.inf fun i => Ideal.span {I i}) = Ideal.span {∏ i ∈ s, I i}
• 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)
• AddSubgroup.noncommSum_mem 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise (Function.onFun AddCommute f)) : (∀ c ∈ t, f c ∈ K) → t.noncommSum f comm ∈ K
• Subgroup.noncommProd_mem 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [Group G] (K : Subgroup G) {ι : Type u_3} {t : Finset ι} {f : ι → G} (comm : (↑t).Pairwise (Function.onFun Commute f)) : (∀ c ∈ t, f c ∈ K) → t.noncommProd f comm ∈ K
• partialSups_disjoint_of_disjoint 📋 Mathlib.Order.PartialSups
  {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] [DistribLattice α] [OrderBot α] (f : ι → α) (h : Pairwise (Function.onFun Disjoint f)) {i j : ι} (hij : i < j) : Disjoint ((partialSups f) i) (f j)
• LinearMap.ker_noncommProd_eq_of_supIndep_ker 📋 Mathlib.LinearAlgebra.FiniteDimensional.Basic
  {K : Type u} {V : Type v} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_1} {f : ι → V →ₗ[K] V} (s : Finset ι) (comm : (↑s).Pairwise (Function.onFun Commute f)) (h : s.SupIndep fun i => LinearMap.ker (f i)) : LinearMap.ker (s.noncommProd f comm) = ⨆ i ∈ s, LinearMap.ker (f i)
• MvPolynomial.vars_sum_of_disjoint 📋 Mathlib.Algebra.MvPolynomial.Variables
  {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R) [DecidableEq σ] (h : Pairwise (Function.onFun Disjoint fun i => (φ i).vars)) : (∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars
• Polynomial.natDegree_sum_eq_of_disjoint 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.natDegree ∘ f))) : (s.sum f).natDegree = s.sup fun i => (f i).natDegree
• Polynomial.degree_sum_eq_of_disjoint 📋 Mathlib.Algebra.Polynomial.Degree.Lemmas
  {R : Type u} {S : Type v} [Semiring R] (f : S → Polynomial R) (s : Finset S) (h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Function.onFun Ne (Polynomial.degree ∘ f))) : (s.sum f).degree = s.sup fun i => (f i).degree
• Ideal.quotientInfToPiQuotient_surj 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_2} [CommRing R] {ι : Type u_3} [Finite ι] {I : ι → Ideal R} (hI : Pairwise (Function.onFun IsCoprime I)) : Function.Surjective ⇑(Ideal.quotientInfToPiQuotient I)
• Ideal.quotientInfRingEquivPiQuotient 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_2} [CommRing R] {ι : Type u_3} [Finite ι] (f : ι → Ideal R) (hf : Pairwise (Function.onFun IsCoprime f)) : R ⧸ ⨅ i, f i ≃+* ((i : ι) → R ⧸ f i)
• Polynomial.pairwise_coprime_X_sub_C 📋 Mathlib.Algebra.Polynomial.RingDivision
  {K : Type u_1} [Field K] {I : Type v} {s : I → K} (H : Function.Injective s) : Pairwise (Function.onFun IsCoprime fun i => Polynomial.X - Polynomial.C (s i))
• Equiv.Perm.mem_support_of_mem_noncommProd_support 📋 Mathlib.GroupTheory.Perm.Support
  {α : Type u_2} {β : Type u_3} [DecidableEq β] [Fintype β] {s : Finset α} {f : α → Equiv.Perm β} {comm : (↑s).Pairwise (Function.onFun Commute f)} {x : β} (hx : x ∈ (s.noncommProd f comm).support) : ∃ a ∈ s, x ∈ (f a).support
• AddSubgroup.eq_zero_of_noncommSum_eq_zero_of_iSupIndep 📋 Mathlib.GroupTheory.NoncommPiCoprod
  {G : Type u_1} [AddGroup G] {ι : Type u_2} (s : Finset ι) (f : ι → G) (comm : (↑s).Pairwise (Function.onFun AddCommute f)) (K : ι → AddSubgroup G) (hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : s.noncommSum f comm = 0) (i : ι) : i ∈ s → f i = 0
• Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep 📋 Mathlib.GroupTheory.NoncommPiCoprod
  {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (f : ι → G) (comm : (↑s).Pairwise (Function.onFun Commute f)) (K : ι → Subgroup G) (hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : s.noncommProd f comm = 1) (i : ι) : i ∈ s → f i = 1
• Subgroup.eq_one_of_noncommProd_eq_one_of_independent 📋 Mathlib.GroupTheory.NoncommPiCoprod
  {G : Type u_1} [Group G] {ι : Type u_2} (s : Finset ι) (f : ι → G) (comm : (↑s).Pairwise (Function.onFun Commute f)) (K : ι → Subgroup G) (hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x) (heq1 : s.noncommProd f comm = 1) (i : ι) : i ∈ s → f i = 1
• Equiv.Perm.cycleFactorsFinset_eq_finset 📋 Mathlib.GroupTheory.Perm.Cycle.Factors
  {α : Type u_2} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} {s : Finset (Equiv.Perm α)} : σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Equiv.Perm.Disjoint), s.noncommProd id ⋯ = σ
• Equiv.Perm.cycleType_eq' 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {σ : Equiv.Perm α} (s : Finset (Equiv.Perm α)) (h1 : ∀ f ∈ s, f.IsCycle) (h2 : (↑s).Pairwise Equiv.Perm.Disjoint) (h0 : s.noncommProd id ⋯ = σ) : σ.cycleType = Multiset.map (Finset.card ∘ Equiv.Perm.support) s.val
• Pairwise.exists_mem_filter_of_disjoint 📋 Mathlib.Order.Filter.Finite
  {α : Type u} {ι : Type u_2} [Finite ι] {l : ι → Filter α} (hd : Pairwise (Function.onFun Disjoint l)) : ∃ s, (∀ (i : ι), s i ∈ l i) ∧ Pairwise (Function.onFun Disjoint s)
• Pairwise.exists_mem_filter_basis_of_disjoint 📋 Mathlib.Order.Filter.Bases.Finite
  {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} (hd : Pairwise (Function.onFun Disjoint l)) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) : ∃ ind, (∀ (i : I), p i (ind i)) ∧ Pairwise (Function.onFun Disjoint fun i => s i (ind i))
• Pairwise.countable_of_isOpen_disjoint 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α} (hd : Pairwise (Function.onFun Disjoint s)) (ho : ∀ (i : ι), IsOpen (s i)) (hne : ∀ (i : ι), (s i).Nonempty) : Countable ι
• pairwise_disjoint_nhds 📋 Mathlib.Topology.Separation.Hausdorff
  {X : Type u_1} [TopologicalSpace X] [T2Space X] : Pairwise (Function.onFun Disjoint nhds)
• subsingleton_of_disjoint_isClopen 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) (h_clopen : ∀ (i : ι), IsClopen (s i)) : Subsingleton ι
• subsingleton_of_disjoint_isOpen_iUnion_eq_univ 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) (h_open : ∀ (i : ι), IsOpen (s i)) (h_Union : ⋃ i, s i = Set.univ) : Subsingleton ι
• subsingleton_of_disjoint_isClosed_iUnion_eq_univ 📋 Mathlib.Topology.Connected.Clopen
  {α : Type u} {ι : Type u_1} [TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α} (h_nonempty : ∀ (i : ι), (s i).Nonempty) (h_disj : Pairwise (Function.onFun Disjoint s)) [Finite ι] (h_closed : ∀ (i : ι), IsClosed (s i)) (h_Union : ⋃ i, s i = Set.univ) : Subsingleton ι
• Submodule.supIndep_torsionBy 📋 Mathlib.Algebra.Module.Torsion
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) : S.SupIndep fun i => Submodule.torsionBy R M (q i)
• Submodule.iSup_torsionBy_eq_torsionBy_prod 📋 Mathlib.Algebra.Module.Torsion
  {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) : ⨆ i ∈ S, Submodule.torsionBy R M (q i) = Submodule.torsionBy R M (∏ i ∈ S, q i)
• Submodule.torsionBy_isInternal 📋 Mathlib.Algebra.Module.Torsion
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [DecidableEq ι] {S : Finset ι} {q : ι → R} (hq : (↑S).Pairwise (Function.onFun IsCoprime q)) (hM : Module.IsTorsionBy R M (∏ i ∈ S, q i)) : DirectSum.IsInternal fun i => Submodule.torsionBy R M (q ↑i)
• Polynomial.separable_prod 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {f : ι → Polynomial R} (h1 : Pairwise (Function.onFun IsCoprime f)) (h2 : ∀ (x : ι), (f x).Separable) : (∏ x, f x).Separable
• disjoint_disjointed 📋 Mathlib.Order.Disjointed
  {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : Pairwise (Function.onFun Disjoint (disjointed f))
• Fintype.exists_disjointed_le 📋 Mathlib.Order.Disjointed
  {α : Type u_1} [GeneralizedBooleanAlgebra α] {ι : Type u_3} [Fintype ι] (f : ι → α) : ∃ g ≤ f, Finset.univ.sup g = Finset.univ.sup f ∧ Pairwise (Function.onFun Disjoint g)
• disjointed_unique' 📋 Mathlib.Order.Disjointed
  {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] {f d : ι → α} (hdisj : Pairwise (Function.onFun Disjoint d)) (hsups : partialSups d = partialSups f) : d = disjointed f
• MeasureTheory.OuterMeasure.iUnion_nat 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {α : Type u_2} (self : MeasureTheory.OuterMeasure α) (s : ℕ → Set α) : Pairwise (Function.onFun Disjoint s) → self.measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), self.measureOf (s i)
• MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {F : Type u_2} {α : outParam (Type u_3)} {inst✝ : FunLike F (Set α) ENNReal} [self : MeasureTheory.OuterMeasureClass F α] (f : F) (s : ℕ → Set α) : Pairwise (Function.onFun Disjoint s) → f (⋃ i, s i) ≤ ∑' (i : ℕ), f (s i)
• MeasureTheory.OuterMeasure.mk 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {α : Type u_2} (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0) (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂) (iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)) : MeasureTheory.OuterMeasure α
• MeasureTheory.OuterMeasureClass.mk 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {F : Type u_2} {α : outParam (Type u_3)} [FunLike F (Set α) ENNReal] (measure_empty : ∀ (f : F), f ∅ = 0) (measure_mono : ∀ (f : F) {s t : Set α}, s ⊆ t → f s ≤ f t) (measure_iUnion_nat_le : ∀ (f : F) (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → f (⋃ i, s i) ≤ ∑' (i : ℕ), f (s i)) : MeasureTheory.OuterMeasureClass F α
• MeasureTheory.OuterMeasure.mk.sizeOf_spec 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {α : Type u_2} [SizeOf α] (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0) (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂) (iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)) : sizeOf { measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } = 1 + sizeOf empty
• MeasureTheory.OuterMeasure.mk.injEq 📋 Mathlib.MeasureTheory.OuterMeasure.Defs
  {α : Type u_2} (measureOf : Set α → ENNReal) (empty : measureOf ∅ = 0) (mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf s₁ ≤ measureOf s₂) (iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf (s i)) (measureOf✝ : Set α → ENNReal) (empty✝ : measureOf✝ ∅ = 0) (mono✝ : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → measureOf✝ s₁ ≤ measureOf✝ s₂) (iUnion_nat✝ : ∀ (s : ℕ → Set α), Pairwise (Function.onFun Disjoint s) → measureOf✝ (⋃ i, s i) ≤ ∑' (i : ℕ), measureOf✝ (s i)) : ({ measureOf := measureOf, empty := empty, mono := mono, iUnion_nat := iUnion_nat } = { measureOf := measureOf✝, empty := empty✝, mono := mono✝, iUnion_nat := iUnion_nat✝ }) = (measureOf = measureOf✝)
• Encodable.iUnion_decode₂_disjoint_on 📋 Mathlib.Logic.Encodable.Lattice
  {α : Type u_1} {β : Type u_2} [Encodable β] {f : β → Set α} (hd : Pairwise (Function.onFun Disjoint f)) : Pairwise (Function.onFun Disjoint fun i => ⋃ b ∈ Encodable.decode₂ β i, f b)
• hasProd_prod_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousMul α] {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)) : HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)
• hasSum_sum_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [ContinuousAdd α] {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α} (hs : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, HasSum (f ∘ Subtype.val) (a i)) : HasSum (f ∘ Subtype.val) (∑ i ∈ s, a i)
• tprod_finset_bUnion_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val)) : ∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x
• tsum_finset_bUnion_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Summable (f ∘ Subtype.val)) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
• Multipliable.tprod_finset_bUnion_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousMul α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Multipliable (f ∘ Subtype.val)) : ∏' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∏ i ∈ s, ∏' (x : ↑(t i)), f ↑x
• Summable.tsum_finset_bUnion_disjoint 📋 Mathlib.Topology.Algebra.InfiniteSum.Basic
  {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} [T2Space α] [ContinuousAdd α] {ι : Type u_4} {s : Finset ι} {t : ι → Set β} (hd : (↑s).Pairwise (Function.onFun Disjoint t)) (hf : ∀ i ∈ s, Summable (f ∘ Subtype.val)) : ∑' (x : ↑(⋃ i ∈ s, t i)), f ↑x = ∑ i ∈ s, ∑' (x : ↑(t i)), f ↑x
• MeasurableSpace.DynkinSystem.has_iUnion_nat 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_4} (self : MeasurableSpace.DynkinSystem α) {f : ℕ → Set α} : Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), self.Has (f i)) → self.Has (⋃ i, f i)
• MeasurableSpace.DynkinSystem.GenerateHas.iUnion 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_3} {s : Set (Set α)} {f : ℕ → Set α} : Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas s (f i)) → MeasurableSpace.DynkinSystem.GenerateHas s (⋃ i, f i)
• MeasurableSpace.DynkinSystem.has_iUnion 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {β : Type u_4} [Countable β] {f : β → Set α} (hd : Pairwise (Function.onFun Disjoint f)) (h : ∀ (i : β), d.Has (f i)) : d.Has (⋃ i, f i)
• MeasurableSpace.DynkinSystem.mk 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_4} (Has : Set α → Prop) (has_empty : Has ∅) (has_compl : ∀ {a : Set α}, Has a → Has aᶜ) (has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)) : MeasurableSpace.DynkinSystem α
• MeasurableSpace.DynkinSystem.GenerateHas.below.iUnion 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_3} {s : Set (Set α)} {motive✝ : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop} {f : ℕ → Set α} (a✝ : Pairwise (Function.onFun Disjoint f)) {a✝¹ : ∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas s (f i)} : (∀ (i : ℕ), ⋯.below) → (∀ (i : ℕ), motive✝ (f i) ⋯) → ⋯.below
• MeasurableSpace.DynkinSystem.mk.sizeOf_spec 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_4} [SizeOf α] (Has : Set α → Prop) (has_empty : Has ∅) (has_compl : ∀ {a : Set α}, Has a → Has aᶜ) (has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)) : sizeOf { Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } = 1 + sizeOf has_empty
• MeasurableSpace.DynkinSystem.mk.injEq 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_4} (Has : Set α → Prop) (has_empty : Has ∅) (has_compl : ∀ {a : Set α}, Has a → Has aᶜ) (has_iUnion_nat : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has (f i)) → Has (⋃ i, f i)) (Has✝ : Set α → Prop) (has_empty✝ : Has✝ ∅) (has_compl✝ : ∀ {a : Set α}, Has✝ a → Has✝ aᶜ) (has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Function.onFun Disjoint f) → (∀ (i : ℕ), Has✝ (f i)) → Has✝ (⋃ i, f i)) : ({ Has := Has, has_empty := has_empty, has_compl := has_compl, has_iUnion_nat := has_iUnion_nat } = { Has := Has✝, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }) = (Has = Has✝)
• MeasurableSpace.induction_on_inter 📋 Mathlib.MeasureTheory.PiSystem
  {α : Type u_3} {m : MeasurableSpace α} {C : (s : Set α) → MeasurableSet s → Prop} {s : Set (Set α)} (h_eq : m = MeasurableSpace.generateFrom s) (h_inter : IsPiSystem s) (empty : C ∅ ⋯) (basic : ∀ (t : Set α) (ht : t ∈ s), C t ⋯) (compl : ∀ (t : Set α) (htm : MeasurableSet t), C t htm → C tᶜ ⋯) (iUnion : ∀ (f : ℕ → Set α), Pairwise (Function.onFun Disjoint f) → ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)), (∀ (i : ℕ), C (f i) ⋯) → C (⋃ i, f i) ⋯) (t : Set α) (ht : MeasurableSet t) : C t ht
• MeasureTheory.OuterMeasure.isCaratheodory_iUnion_of_disjoint 📋 Mathlib.MeasureTheory.OuterMeasure.Caratheodory
  {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m.IsCaratheodory (⋃ i, s i)
• MeasureTheory.OuterMeasure.f_iUnion 📋 Mathlib.MeasureTheory.OuterMeasure.Caratheodory
  {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
• MeasureTheory.OuterMeasure.iUnion_eq_of_caratheodory 📋 Mathlib.MeasureTheory.OuterMeasure.Caratheodory
  {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (s i)) (hd : Pairwise (Function.onFun Disjoint s)) : m (⋃ i, s i) = ∑' (i : ℕ), m (s i)
• MeasureTheory.OuterMeasure.isCaratheodory_sum 📋 Mathlib.MeasureTheory.OuterMeasure.Caratheodory
  {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), m.IsCaratheodory (s i)) (hd : Pairwise (Function.onFun Disjoint s)) {t : Set α} {n : ℕ} : ∑ i ∈ Finset.range n, m (t ∩ s i) = m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
• MeasureTheory.inducedOuterMeasure_eq 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs
• MeasureTheory.inducedOuterMeasure_eq_extend 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : (MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s
• MeasureTheory.extend_iUnion_le_tsum_nat 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) (s : ℕ → Set α) : MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
• MeasureTheory.extend_mono 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ s₂ : Set α} (h₁ : MeasurableSet s₁) (hs : s₁ ⊆ s₂) : MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂
• MeasureTheory.extend_iUnion 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {β : Type u_2} [Countable β] {f : β → Set α} (hd : Pairwise (Function.onFun Disjoint f)) (hm : ∀ (i : β), P (f i)) : MeasureTheory.extend m (⋃ i, f i) = ∑' (i : β), MeasureTheory.extend m (f i)
• MeasureTheory.extend_union 📋 Mathlib.MeasureTheory.OuterMeasure.Induced
  {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ s₂ : Set α} (hd : Disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) : MeasureTheory.extend m (s₁ ∪ s₂) = MeasureTheory.extend m s₁ + MeasureTheory.extend m s₂
• MeasureTheory.Measure.m_iUnion 📋 Mathlib.MeasureTheory.Measure.MeasureSpaceDef
  {α : Type u_6} [MeasurableSpace α] (self : MeasureTheory.Measure α) ⦃f : ℕ → Set α⦄ : (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → self.toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), self.toOuterMeasure (f i)
• MeasureTheory.Measure.ofMeasurable 📋 Mathlib.MeasureTheory.Measure.MeasureSpaceDef
  {α : Type u_1} [MeasurableSpace α] (m : (s : Set α) → MeasurableSet s → ENNReal) (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) : MeasureTheory.Measure α

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

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

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

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

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

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

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

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

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

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

Source code

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

This is Loogle revision 19971e9 serving mathlib revision f167e8d