Loogle!

Result

Found 1332 declarations whose name contains "iUnion". Of these, only the first 200 are shown.

Set.iUnion_delab 📋 Mathlib.Order.SetNotation
: Lean.PrettyPrinter.Delaborator.Delab
Set.iUnion 📋 Mathlib.Order.SetNotation
{α : Type u} {ι : Sort v} (s : ι → Set α) : Set α
Set.iSup_eq_iUnion 📋 Mathlib.Order.SetNotation
{α : Type u} {ι : Sort v} (s : ι → Set α) : iSup s = Set.iUnion s
Set.mem_iUnion 📋 Mathlib.Order.SetNotation
{α : Type u} {ι : Sort v} {x : α} {s : ι → Set α} : x ∈ ⋃ i, s i ↔ ∃ i, x ∈ s i
Set.iUnion_true 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s : True → Set α} : Set.iUnion s = s trivial
Set.iUnion_const 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) : ⋃ x, s = s
Set.nonempty_of_nonempty_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι
Set.iUnion_false 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s : False → Set α} : Set.iUnion s = ∅
Set.iUnion_nonempty_self 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (s : Set α) : ⋃ (_ : s.Nonempty), s = s
Set.iUnion_le_nat 📋 Mathlib.Data.Set.Lattice
: ⋃ n, {i | i ≤ n} = Set.univ
Set.iUnion_of_singleton 📋 Mathlib.Data.Set.Lattice
(α : Type u_12) : ⋃ x, {x} = Set.univ
Set.iUnion_empty 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} : ⋃ x, ∅ = ∅
Set.subset_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : ι → Set β) (i : ι) : s i ⊆ ⋃ i, s i
Set.nonempty_of_nonempty_iUnion_eq_univ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = Set.univ) : Nonempty ι
Set.sigmaToiUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (t : α → Set β) (x : (i : α) × ↑(t i)) : ↑(⋃ i, t i)
Set.iUnion_of_empty 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} [IsEmpty ι] (s : ι → Set α) : ⋃ i, s i = ∅
Set.nonempty_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} : (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty
Set.iUnion_subset_iUnion_const 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {s : Set α} (h : ι → ι₂) : ⋃ x, s ⊆ ⋃ x, s
Set.iUnion_singleton_eq_range 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (f : α → β) : ⋃ x, {f x} = Set.range f
Set.iInter_subset_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} [Nonempty ι] {s : ι → Set α} : ⋂ i, s i ⊆ ⋃ i, s i
Set.iUnion_plift_down 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (f : ι → Set α) : ⋃ i, f i.down = ⋃ i, f i
Set.iUnion_eq_if 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {p : Prop} [Decidable p] (s : Set α) : ⋃ (_ : p), s = if p then s else ∅
Set.iUnion_plift_up 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (f : PLift ι → Set α) : ⋃ i, f { down := i } = ⋃ i, f i
Set.sigmaToiUnion_surjective 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (t : α → Set β) : Function.Surjective (Set.sigmaToiUnion t)
Set.union_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s₁ s₂ : Set α} : s₁ ∪ s₂ = ⋃ b, bif b then s₁ else s₂
Set.iUnion_eq_const 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} [Nonempty ι] {f : ι → Set α} {s : Set α} (hf : ∀ (i : ι), f i = s) : ⋃ i, f i = s
Set.sInter_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (s : ι → Set (Set α)) : ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i
Set.sUnion_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (s : ι → Set (Set α)) : ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i
Set.iUnion_setOf 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (P : ι → α → Prop) : ⋃ i, {x | P i x} = {x | ∃ i, P i x}
Set.iUnion_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α} (h : ∀ (i : ι), s i ⊆ t) : ⋃ i, s i ⊆ t
Set.subset_iUnion_of_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : Set α} {t : ι → Set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i
Function.Surjective.iUnion_comp 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → ι₂} (hf : Function.Surjective f) (g : ι₂ → Set α) : ⋃ x, g (f x) = ⋃ y, g y
Set.iUnion_subset_iff 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {t : Set α} : ⋃ i, s i ⊆ t ↔ ∀ (i : ι), s i ⊆ t
Set.mem_iUnion_of_mem 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} {a : α} (i : ι) (ha : a ∈ s i) : a ∈ ⋃ i, s i
Set.biUnion_self 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (s : Set α) : ⋃ x ∈ s, s = s
Set.compl_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : ι → Set β) : (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ
Set.iInter_eq_compl_iUnion_compl 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : ι → Set β) : ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ
Set.iUnion_eq_compl_iInter_compl 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : ι → Set β) : ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ
Set.iUnion_eq_univ_iff 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {f : ι → Set α} : ⋃ i, f i = Set.univ ↔ ∀ (x : α), ∃ i, x ∈ f i
Set.iUnion₂_subset_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (κ : ι → Sort u_12) (s : ι → Set α) : ⋃ i, ⋃ x, s i ⊆ ⋃ i, s i
Set.iUnion_congr 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s t : ι → Set α} (h : ∀ (i : ι), s i = t i) : ⋃ i, s i = ⋃ i, t i
Set.iUnion_eq_dif 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {p : Prop} [Decidable p] (s : p → Set α) : ⋃ (h : p), s h = if h : p then s h else ∅
Set.iUnion_eq_empty 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s : ι → Set α} : ⋃ i, s i = ∅ ↔ ∀ (i : ι), s i = ∅
Set.iUnion_mono'' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s t : ι → Set α} (h : ∀ (i : ι), s i ⊆ t i) : Set.iUnion s ⊆ Set.iUnion t
Set.iUnion_comm 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (s : ι → ι' → Set α) : ⋃ i, ⋃ i', s i i' = ⋃ i', ⋃ i, s i i'
Set.iUnion_of_singleton_coe 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (s : Set α) : ⋃ i, {↑i} = s
Set.iUnion_option 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Type u_12} (s : Option ι → Set α) : ⋃ o, s o = s none ∪ ⋃ i, s (some i)
Set.range_sigma_eq_iUnion_range 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (f : Sigma γ → β) : Set.range f = ⋃ a, Set.range fun b => f ⟨a, b⟩
Set.subset_iUnion₂ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i) : s i j ⊆ ⋃ i', ⋃ j', s i' j'
Set.iUnion_diff 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β) : (⋃ i, t i) \ s = ⋃ i, t i \ s
Set.iUnion_iInter_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {s : ι → ι' → Set α} : ⋃ j, ⋂ i, s i j ⊆ ⋂ i, ⋃ j, s i j
Set.iUnion_inter 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s
Set.inter_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β) : s ∩ ⋃ i, t i = ⋃ i, s ∩ t i
Set.iUnion_and 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {p q : Prop} (s : p ∧ q → Set α) : ⋃ (h : p ∧ q), s h = ⋃ (hp : p), ⋃ (hq : q), s ⋯
Set.iUnion_congr_Prop 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q) (f : ∀ (x : q), f₁ ⋯ = f₂ x) : Set.iUnion f₁ = Set.iUnion f₂
Set.iUnion_iUnion_eq_left 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = b → Set α} : ⋃ x, ⋃ (h : x = b), s x h = s b ⋯
Set.iUnion_iUnion_eq_right 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → b = x → Set α} : ⋃ x, ⋃ (h : b = x), s x h = s b ⋯
Set.iUnion_mono 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {s t : ι → Set α} (h : ∀ (i : ι), s i ⊆ t i) : ⋃ i, s i ⊆ ⋃ i, t i
Set.biUnion_const 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) (t : Set β) : ⋃ a ∈ s, t = t
Set.biUnion_of_singleton 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (s : Set α) : ⋃ x ∈ s, {x} = s
Set.diff_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β) : s \ ⋃ i, t i = ⋂ i, s \ t i
Set.iUnion_union 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s
Set.union_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [Nonempty ι] (s : Set β) (t : ι → Set β) : s ∪ ⋃ i, t i = ⋃ i, s ∪ t i
Set.insert_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [Nonempty ι] (x : β) (t : ι → Set β) : insert x (⋃ i, t i) = ⋃ i, insert x (t i)
Set.sUnion_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s : Set (Set α)} : ⋃₀ s = ⋃ i, ↑i
Set.iUnion_exists 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {p : ι → Prop} {f : Exists p → Set α} : ⋃ (x : Exists p), f x = ⋃ i, ⋃ (h : p i), f ⋯
Set.iUnion_psigma 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : PSigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩
Set.iUnion_sigma 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : Sigma γ → Set β) : ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩
Set.pi_iUnion_eq_iInter_pi 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {π : α → Type u_12} {α' : Type u_13} (s : α' → Set α) (t : (a : α) → Set (π a)) : (⋃ i, s i).pi t = ⋂ i, (s i).pi t
Set.directedOn_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {r : α → α → Prop} {f : ι → Set α} (hd : Directed (fun x1 x2 => x1 ⊆ x2) f) (h : ∀ (x : ι), DirectedOn r (f x)) : DirectedOn r (⋃ x, f x)
Set.iUnion_congr_of_surjective 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂) (h1 : Function.Surjective h) (h2 : ∀ (x : ι), g (h x) = f x) : ⋃ x, f x = ⋃ y, g y
Set.iUnion_insert_eq_range_union_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Type u_12} (x : ι → β) (t : ι → Set β) : ⋃ i, insert (x i) (t i) = Set.range x ∪ ⋃ i, t i
Set.iUnion_mono' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {s : ι → Set α} {t : ι₂ → Set α} (h : ∀ (i : ι), ∃ j, s i ⊆ t j) : ⋃ i, s i ⊆ ⋃ i, t i
sSup_iUnion 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} [CompleteLattice β] (t : ι → Set β) : sSup (⋃ i, t i) = ⨆ i, sSup (t i)
Set.biUnion_univ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ x ∈ Set.univ, s x = ⋃ x, s x
Set.iUnion_ge_eq_iUnion_nat_add 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (u : ℕ → Set α) (n : ℕ) : ⋃ i, ⋃ (_ : i ≥ n), u i = ⋃ i, u (i + n)
Set.biUnion_gt_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} [LT α] [NoMinOrder α] {s : α → Set β} : ⋃ n, ⋃ m, ⋃ (_ : m > n), s m = ⋃ n, s n
Set.biUnion_lt_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} [LT α] [NoMaxOrder α] {s : α → Set β} : ⋃ n, ⋃ m, ⋃ (_ : m < n), s m = ⋃ n, s n
Set.iUnion_union_distrib 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s t : ι → Set β) : ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i
Set.sUnion_eq_biUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {s : Set (Set α)} : ⋃₀ s = ⋃ i ∈ s, i
Set.biUnion_ge_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋃ n, ⋃ m, ⋃ (_ : m ≥ n), s m = ⋃ n, s n
Set.biUnion_le_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} [Preorder α] {s : α → Set β} : ⋃ n, ⋃ m, ⋃ (_ : m ≤ n), s m = ⋃ n, s n
Set.iUnion_psigma' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia, s ia.fst ia.snd
Set.iUnion_sigma' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : α → Type u_12} (s : (i : α) → γ i → Set β) : ⋃ i, ⋃ a, s i a = ⋃ ia, s ia.fst ia.snd
Set.iUnion₂_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α} (h : ∀ (i : ι) (j : κ i), s i j ⊆ t) : ⋃ i, ⋃ j, s i j ⊆ t
Set.subset_iUnion₂_of_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : Set α} {t : (i : ι) → κ i → Set α} (i : ι) (j : κ i) (h : s ⊆ t i j) : s ⊆ ⋃ i, ⋃ j, t i j
Set.union_iUnion_nat_succ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (u : ℕ → Set α) : u 0 ∪ ⋃ i, u (i + 1) = ⋃ i, u i
Set.iUnion_inter_subset 📋 Mathlib.Data.Set.Lattice
{ι : Sort u_12} {α : Type u_13} {s t : ι → Set α} : ⋃ i, s i ∩ t i ⊆ (⋃ i, s i) ∩ ⋃ i, t i
Set.iUnion₂_subset_iff 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {t : Set α} : ⋃ i, ⋃ j, s i j ⊆ t ↔ ∀ (i : ι) (j : κ i), s i j ⊆ t
Set.mem_iUnion₂_of_mem 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} {a : α} {i : ι} (j : κ i) (ha : a ∈ s i j) : a ∈ ⋃ i, ⋃ j, s i j
Set.iUnion_or 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {p q : Prop} (s : p ∨ q → Set α) : ⋃ (h : p ∨ q), s h = (⋃ (i : p), s ⋯) ∪ ⋃ (j : q), s ⋯
Set.iUnion_sum 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α ⊕ β → Set γ} : ⋃ x, s x = (⋃ x, s (Sum.inl x)) ∪ ⋃ x, s (Sum.inr x)
Set.biUnion_empty 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ x ∈ ∅, s x = ∅
Set.iUnion_subtype 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (p : α → Prop) (s : { x // p x } → Set β) : ⋃ x, s x = ⋃ x, ⋃ (hx : p x), s ⟨x, hx⟩
Set.biUnion_singleton 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (a : α) (s : α → Set β) : ⋃ x ∈ {a}, s x = s a
Set.iUnion₂_eq_univ_iff 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set α} : ⋃ i, ⋃ j, s i j = Set.univ ↔ ∀ (a : α), ∃ i j, a ∈ s i j
Set.subset_biUnion_of_mem 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s : Set α} {u : α → Set β} {x : α} (xs : x ∈ s) : u x ⊆ ⋃ x ∈ s, u x
Set.compl_iUnion₂ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) : (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ
Set.iUnion_image_preimage_sigma_mk_eq_self 📋 Mathlib.Data.Set.Lattice
{ι : Type u_12} {σ : ι → Type u_13} (s : Set (Sigma σ)) : ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s
Set.mem_iUnion₂ 📋 Mathlib.Data.Set.Lattice
{γ : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_8} {x : γ} {s : (i : ι) → κ i → Set γ} : x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j
Set.nonempty_biUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {t : Set α} {s : α → Set β} : (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty
Monotone.iUnion_nat_add 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {f : ℕ → Set α} (hf : Monotone f) (k : ℕ) : ⋃ n, f (n + k) = ⋃ n, f n
Set.iUnion_univ_pi 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {π : α → Type u_12} {ι : α → Type u_13} (t : (a : α) → ι a → Set (π a)) : (⋃ x, Set.univ.pi fun a => t a (x a)) = Set.univ.pi fun a => ⋃ j, t a j
Set.iUnion₂_inter 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (t : Set α) : (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t
Set.inter_iUnion₂ 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α) (t : (i : ι) → κ i → Set α) : s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j
Set.iUnion_range_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} (C : ι → Set α) {f : (x : ι) → β → ↑(C x)} (hf : ∀ (x : ι), Function.Surjective (f x)) : (⋃ y, Set.range fun x => ↑(f x y)) = ⋃ x, C x
Set.iUnion₂_congr 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α} (h : ∀ (i : ι) (j : κ i), s i j = t i j) : ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, t i j
Set.iUnion_eq_range_psigma 📋 Mathlib.Data.Set.Lattice
{β : Type u_2} {ι : Sort u_5} (s : ι → Set β) : ⋃ i, s i = Set.range fun a => ↑a.snd
Set.iUnion_eq_range_sigma 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s : α → Set β) : ⋃ i, s i = Set.range fun a => ↑a.snd
Set.mem_biUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) : y ∈ ⋃ x ∈ s, t x
Set.iUnion_coe_set 📋 Mathlib.Data.Set.Lattice
{α : Type u_12} {β : Type u_13} (s : Set α) (f : ↑s → Set β) : ⋃ i, f i = ⋃ i, ⋃ (h : i ∈ s), f ⟨i, h⟩
Set.iUnion_nonempty_index 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s : Set α) (t : s.Nonempty → Set β) : ⋃ (h : s.Nonempty), t h = ⋃ x, ⋃ (h : x ∈ s), t ⋯
Set.iUnion₂_mono 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} {s t : (i : ι) → κ i → Set α} (h : ∀ (i : ι) (j : κ i), s i j ⊆ t i j) : ⋃ i, ⋃ j, s i j ⊆ ⋃ i, ⋃ j, t i j
Set.iUnion_iInter_ge_nat_add 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} (f : ℕ → Set α) (k : ℕ) : ⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f (i + k) = ⋃ n, ⋂ i, ⋂ (_ : i ≥ n), f i
Set.iUnion_ite 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [DecidablePred p] (f g : ι → Set α) : (⋃ i, if p i then f i else g i) = (⋃ i, ⋃ (_ : p i), f i) ∪ ⋃ i, ⋃ (_ : ¬p i), g i
Set.biInter_subset_biUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s : Set α} (hs : s.Nonempty) {t : α → Set β} : ⋂ x ∈ s, t x ⊆ ⋃ x ∈ s, t x
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.iUnion₂_comm 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_8} {κ' : ι' → Sort u_11} (s : (i : ι) → κ i → (i' : ι') → κ' i' → Set α) : ⋃ i, ⋃ j, ⋃ i', ⋃ j', s i j i' j' = ⋃ i', ⋃ j', ⋃ i, ⋃ j, s i j i' j'
Set.biUnion_pair 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (a b : α) (s : α → Set β) : ⋃ x ∈ {a, b}, s x = s a ∪ s b
Set.biUnion_subset_biUnion_left 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s s' : Set α} {t : α → Set β} (h : s ⊆ s') : ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x
Set.biUnion_ge 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Type u_12} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋃ j, ⋃ (_ : j ≥ i), s j = s i ∪ ⋃ j, ⋃ (_ : j > i), s j
Set.biUnion_le 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Type u_12} [PartialOrder ι] (s : ι → Set α) (i : ι) : ⋃ j, ⋃ (_ : j ≤ i), s j = (⋃ j, ⋃ (_ : j < i), s j) ∪ s i
Set.iUnion₂_mono' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_8} {κ' : ι' → Sort u_11} {s : (i : ι) → κ i → Set α} {t : (i' : ι') → κ' i' → Set α} (h : ∀ (i : ι) (j : κ i), ∃ i' j', s i j ⊆ t i' j') : ⋃ i, ⋃ j, s i j ⊆ ⋃ i', ⋃ j', t i' j'
Set.biInter_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (t : α → Set β) : ⋂ x ∈ ⋃ i, s i, t x = ⋂ i, ⋂ x ∈ s i, t x
Set.biUnion_eq_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s : Set α) (t : (x : α) → x ∈ s → Set β) : ⋃ x, ⋃ (h : x ∈ s), t x h = ⋃ x, t ↑x ⋯
Set.biUnion_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} (s : ι → Set α) (t : α → Set β) : ⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x
Set.iUnion_dite 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} (p : ι → Prop) [DecidablePred p] (f : (i : ι) → p i → Set α) (g : (i : ι) → ¬p i → Set α) : (⋃ i, if h : p i then f i h else g i h) = (⋃ i, ⋃ (h : p i), f i h) ∪ ⋃ i, ⋃ (h : ¬p i), g i h
Set.iUnion_iUnion_eq_or_left 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α} : ⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯
Set.biUnion_and 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι → Prop) (q : ι → ι' → Prop) (s : (x : ι) → (y : ι') → p x ∧ q x y → Set α) : ⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯
Set.biUnion_and' 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι' → Prop) (q : ι → ι' → Prop) (s : (x : ι) → (y : ι') → p y ∧ q x y → Set α) : ⋃ x, ⋃ y, ⋃ (h : p y ∧ q x y), s x y h = ⋃ y, ⋃ (hy : p y), ⋃ x, ⋃ (hx : q x y), s x y ⋯
Set.biUnion_insert 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (a : α) (s : Set α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x
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.biUnion_mono 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {s s' : Set α} {t t' : α → Set β} (hs : s' ⊆ s) (h : ∀ x ∈ s, t x ⊆ t' x) : ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x
Set.iUnion_inter_of_antitone 📋 Mathlib.Data.Set.Lattice
{ι : Type u_12} {α : Type u_13} [Preorder ι] [IsCodirectedOrder ι] {s t : ι → Set α} (hs : Antitone s) (ht : Antitone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
Set.iUnion_inter_of_monotone 📋 Mathlib.Data.Set.Lattice
{ι : Type u_12} {α : Type u_13} [Preorder ι] [IsDirectedOrder ι] {s t : ι → Set α} (hs : Monotone s) (ht : Monotone t) : ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i
iInf_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨅ a ∈ ⋃ i, s i, f a = ⨅ i, ⨅ a ∈ s i, f a
iSup_iUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} [CompleteLattice β] (s : ι → Set α) (f : α → β) : ⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a
Set.biUnion_union 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (s t : Set α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x
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_diff_biUnion_subset 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {β : Type u_2} (t : α → Set β) (s₁ s₂ : Set α) : (⋃ x ∈ s₁, t x) \ ⋃ x ∈ s₂, t x ⊆ ⋃ x ∈ s₁ \ s₂, t x
Set.iUnion_range_eq_sUnion 📋 Mathlib.Data.Set.Lattice
{α : Type u_12} {β : Type u_13} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s} (hf : ∀ (s : ↑C), Function.Surjective (f s)) : (⋃ y, Set.range fun s => ↑(f s y)) = ⋃₀ C
Set.biUnion_univ_pi 📋 Mathlib.Data.Set.Lattice
{α : Type u_1} {π : α → Type u_12} {ι : α → Type u_13} (s : (a : α) → Set (ι a)) (t : (a : α) → ι a → Set (π a)) : (⋃ x ∈ Set.univ.pi s, Set.univ.pi fun a => t a (x a)) = Set.univ.pi fun a => ⋃ j ∈ s a, t a 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
sInf_iUnion_Ici 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
{α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) : sInf (⋃ i, Set.Ici (f i)) = ⨅ i, f i
sSup_iUnion_Iic 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
{α : Type u_1} {ι : Sort u_4} [ConditionallyCompleteLinearOrder α] (f : ι → α) : sSup (⋃ i, Set.Iic (f i)) = ⨆ i, f i
Finset.biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : α → Finset β) : Finset β
Finset.biUnion_singleton_eq_self 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {s : Finset α} [DecidableEq α] : s.biUnion singleton = s
Finset.biUnion_empty 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {t : α → Finset β} [DecidableEq β] : ∅.biUnion t = ∅
Finset.disjiUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} (s : Finset α) (t : α → Finset β) (hf : (↑s).PairwiseDisjoint t) : Finset β
Finset.singleton_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {t : α → Finset β} [DecidableEq β] {a : α} : {a}.biUnion t = t a
Finset.disjiUnion_empty 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} (t : α → Finset β) : ∅.disjiUnion t ⋯ = ∅
Finset.biUnion_singleton 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] {f : α → β} : (s.biUnion fun a => {f a}) = Finset.image f s
Finset.subset_biUnion_of_mem 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} [DecidableEq β] (u : α → Finset β) {x : α} (xs : x ∈ s) : u x ⊆ s.biUnion u
Finset.Nonempty.biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] (hs : s.Nonempty) (ht : ∀ x ∈ s, (t x).Nonempty) : (s.biUnion t).Nonempty
Finset.biUnion_nonempty 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] : (s.biUnion t).Nonempty ↔ ∃ x ∈ s, (t x).Nonempty
Finset.biUnion_val 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : α → Finset β) : (s.biUnion t).val = (s.val.bind fun a => (t a).val).dedup
Finset.biUnion_subset_biUnion_of_subset_left 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} [DecidableEq β] (t : α → Finset β) (h : s₁ ⊆ s₂) : s₁.biUnion t ⊆ s₂.biUnion t
Finset.erase_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → Finset β) (s : Finset α) (b : β) : (s.biUnion f).erase b = s.biUnion fun x => (f x).erase b
Finset.image_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} : (Finset.image f s).biUnion t = s.biUnion fun a => t (f a)
Finset.filter_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] : Finset.filter p (s.biUnion f) = s.biUnion fun a => Finset.filter p (f a)
Finset.image_biUnion_filter_eq 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] (s : Finset β) (g : β → α) : ((Finset.image g s).biUnion fun a => {c ∈ s | g c = a}) = s
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.biUnion_image 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} : Finset.image f (s.biUnion t) = s.biUnion fun a => Finset.image f (t a)
Finset.biUnion_subset 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] {s' : Finset β} : s.biUnion t ⊆ s' ↔ ∀ x ∈ s, t x ⊆ s'
Finset.biUnion_subset_iff_forall_subset 📋 Mathlib.Data.Finset.Union
{α : Type u_4} {β : Type u_5} [DecidableEq β] {s : Finset α} {t : Finset β} {f : α → Finset β} : s.biUnion f ⊆ t ↔ ∀ x ∈ s, f x ⊆ t
Finset.biUnion_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq β] [DecidableEq γ] (s : Finset α) (f : α → Finset β) (g : β → Finset γ) : (s.biUnion f).biUnion g = s.biUnion fun a => (f a).biUnion g
Finset.biUnion_inter 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β) : s.biUnion f ∩ t = s.biUnion fun x => f x ∩ t
Finset.inter_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (t : Finset β) (s : Finset α) (f : α → Finset β) : t ∩ s.biUnion f = s.biUnion fun x => t ∩ f x
Finset.biUnion_insert 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] [DecidableEq α] {a : α} : (insert a s).biUnion t = t a ∪ s.biUnion t
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.disjoint_biUnion_left 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β) : Disjoint (s.biUnion f) t ↔ ∀ i ∈ s, Disjoint (f i) t
Finset.disjoint_biUnion_right 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset β) (t : Finset α) (f : α → Finset β) : Disjoint s (t.biUnion f) ↔ ∀ i ∈ t, Disjoint s (f i)
Finset.mem_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a
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.biUnion_mono 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t₁ t₂ : α → Finset β} [DecidableEq β] (h : ∀ a ∈ s, t₁ a ⊆ t₂ a) : s.biUnion t₁ ⊆ s.biUnion t₂
Finset.biUnion_congr 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : α → Finset β} [DecidableEq β] (hs : s₁ = s₂) (ht : ∀ a ∈ s₁, t₁ a = t₂ a) : s₁.biUnion t₁ = s₂.biUnion t₂
Finset.biUnion_filter_eq_of_maps_to 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} [DecidableEq β] [DecidableEq α] {s : Finset α} {t : Finset β} {f : α → β} (h : ∀ x ∈ s, f x ∈ t) : (t.biUnion fun a => {c ∈ s | f c = a}) = s
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.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.filter_disjiUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → Finset β) (h : (↑s).PairwiseDisjoint f) (p : β → Prop) [DecidablePred p] : Finset.filter p (s.disjiUnion f h) = s.disjiUnion (fun a => Finset.filter p (f a)) ⋯
Finset.coe_biUnion 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [DecidableEq β] : ↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)
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.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.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.disjiUnion.congr_simp 📋 Mathlib.Data.Finset.Union
{α : Type u_1} {β : Type u_2} (s s✝ : Finset α) (e_s : s = s✝) (t t✝ : α → Finset β) (e_t : t = t✝) (hf : (↑s).PairwiseDisjoint t) : s.disjiUnion t hf = s✝.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.product_eq_biUnion 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = s.biUnion fun a => Finset.image (fun b => (a, b)) t
Finset.product_eq_biUnion_right 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = t.biUnion fun b => Finset.image (fun a => (a, b)) s
Finset.product_biUnion 📋 Mathlib.Data.Finset.Prod
{α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) : (s ×ˢ t).biUnion f = s.biUnion fun a => t.biUnion fun b => f (a, b)
Set.iUnion.eq_1 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u} {ι : Sort v} (s : ι → Set α) : Set.iUnion s = iSup s
Set.range_eq_iUnion 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {ι : Sort u_9} (f : ι → α) : Set.range f = ⋃ i, {f i}
Set.surjOn_iUnion 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} {f : α → β} (H : ∀ (i : ι), Set.SurjOn f s (t i)) : Set.SurjOn f s (⋃ i, t i)
Set.mapsTo_iUnion 📋 Mathlib.Data.Set.Lattice.Image
{α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : Set β} {f : α → β} : Set.MapsTo f (⋃ i, s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

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

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

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

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

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

Source code

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

This is Loogle revision 6ff4759 serving mathlib revision c3a9c0b