Loogle!

Result

Found 26 declarations mentioning Finset.disjiUnion.

• Finset.disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (hf : (↑s).PairwiseDisjoint t) : Finset β
• Finset.disjiUnion_eq_biUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (hf : (↑s).PairwiseDisjoint f) : s.disjiUnion f hf = s.biUnion f
• Finset.disjiUnion_val 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).val = s.val.bind fun a => (t a).val
• Finset.singleton_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {t : α → Finset β} (a : α) {h : (↑{a}).PairwiseDisjoint t} : {a}.disjiUnion t h = t a
• Finset.mem_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {b : β} {h : (↑s).PairwiseDisjoint t} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a
• Finset.disjiUnion_filter_eq_of_maps_to 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) : t.disjiUnion (fun a => {x ∈ s | f x = a}) ⋯ = s
• Finset.disjiUnion_filter_eq 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : Finset β) (f : α → β) : t.disjiUnion (fun a => {x ∈ s | f x = a}) ⋯ = {c ∈ s | f c ∈ t}
• Finset.coe_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} {h : (↑s).PairwiseDisjoint t} : ↑(s.disjiUnion t h) = ⋃ x ∈ ↑s, ↑(t x)
• Finset.sUnion_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {f : α → Finset (Set β)} (I : Finset α) (hf : (↑I).PairwiseDisjoint f) : ⋃₀ ↑(I.disjiUnion f hf) = ⋃ a ∈ I, ⋃₀ ↑(f a)
• Finset.fold_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {f : α → β} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {ι : Type u_4} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h : (↑s).PairwiseDisjoint t) : Finset.fold op (Finset.fold op b₀ b s) f (s.disjiUnion t h) = Finset.fold op b₀ (fun i => Finset.fold op (b i) f (t i)) s
• Finset.disjiUnion_empty 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} (t : α → Finset β) : ∅.disjiUnion t ⋯ = ∅
• 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)) ⋯
• Finset.map_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ} {h : (↑(Finset.map f s)).PairwiseDisjoint t} : (Finset.map f s).disjiUnion t h = s.disjiUnion (fun a => t (f a)) ⋯
• Finset.disjiUnion_cons 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} (a : α) (s : Finset α) (ha : a ∉ s) (f : α → Finset β) (H : (↑(Finset.cons a s ha)).PairwiseDisjoint f) : (Finset.cons a s ha).disjiUnion f H = (f a).disjUnion (s.disjiUnion f ⋯) ⋯
• Finset.disjiUnion_disjiUnion 📋 Mathlib.Data.Finset.Union
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (f : α → Finset β) (g : β → Finset γ) (h1 : (↑s).PairwiseDisjoint f) (h2 : (↑(s.disjiUnion f h1)).PairwiseDisjoint g) : (s.disjiUnion f h1).disjiUnion g h2 = s.attach.disjiUnion (fun a => (f ↑a).disjiUnion g ⋯) ⋯
• Finset.card_disjiUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {M : Type u_4} (s : Finset ι) (t : ι → Finset M) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).card = ∑ a ∈ s, (t a).card
• Finset.prod_disjiUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι) (h : (↑s).PairwiseDisjoint t) : ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
• Finset.sum_disjiUnion 📋 Mathlib.Algebra.BigOperators.Group.Finset.Basic
  {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι) (h : (↑s).PairwiseDisjoint t) : ∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x
• Finset.disjiUnion_map_sigma_mk 📋 Mathlib.Data.Finset.Sigma
  {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : s.disjiUnion (fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
• Finset.powerset_card_disjiUnion 📋 Mathlib.Data.Finset.Powerset
  {α : Type u_1} (s : Finset α) : s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) ⋯
• Finsupp.uncurry.eq_1 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {β : Type u_2} {M : Type u_5} [Zero M] (f : α →₀ β →₀ M) : f.uncurry = { support := f.support.disjiUnion (fun a => Finset.map (Function.Embedding.sectR a β) (f a).support) ⋯, toFun := fun x => (f x.1) x.2, mem_support_toFun := ⋯ }
• Finset.dens_disjiUnion 📋 Mathlib.Algebra.BigOperators.Field
  {α : Type u_3} {β : Type u_4} [Fintype β] (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens
• Finset.product_self_eq_disjiUnion_perm 📋 Mathlib.GroupTheory.Perm.Cycle.Basic
  {α : Type u_2} {f : Equiv.Perm α} {s : Finset α} (hf : f.IsCycleOn ↑s) : s ×ˢ s = (Finset.range s.card).disjiUnion (fun k => Finset.map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯
• Finset.piAntidiag_cons 📋 Mathlib.Algebra.Order.Antidiag.Pi
  {ι : Type u_1} {μ : Type u_2} [DecidableEq ι] [AddCancelCommMonoid μ] [Finset.HasAntidiagonal μ] [DecidableEq μ] {i : ι} {s : Finset ι} (hi : i ∉ s) (n : μ) : (Finset.cons i s hi).piAntidiag n = (Finset.antidiagonal n).disjiUnion (fun p => Finset.map (addRightEmbedding fun t => if t = i then p.1 else 0) (s.piAntidiag p.2)) ⋯
• SimpleGraph.finsetWalkLengthLT.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
  {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : G.finsetWalkLengthLT n u v = (Finset.range n).disjiUnion (fun l => G.finsetWalkLength l u v) ⋯
• SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset 📋 Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
  {V : Type u} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {G' : SimpleGraph V} (h : G ≤ G') (c' : G'.ConnectedComponent) [Fintype ↑c'.supp] [DecidablePred fun c => c.supp ⊆ c'.supp] : {c | c.supp ⊆ c'.supp}.disjiUnion (fun c => c.supp.toFinset) ⋯ = c'.supp.toFinset

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 40fea08