Loogle!
Result
Found 1084 definitions 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} → (ι → 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_4} [inst : Nonempty ι] (s : Set β), ⋃ x, s = s - Set.nonempty_of_nonempty_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α}, (⋃ 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_of_singleton Mathlib.Data.Set.Lattice
∀ (α : Type u_11), ⋃ x, {x} = Set.univ - Set.iUnion_empty Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4}, ⋃ x, ∅ = ∅ - Set.subset_iUnion Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β) (i : ι), s i ⊆ ⋃ i, s i - Set.iUnion.eq_1 Mathlib.Data.Set.Lattice
∀ {α : Type u} {ι : Sort v} (s : ι → Set α), Set.iUnion s = iSup s - Set.nonempty_of_nonempty_iUnion_eq_univ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} [inst : Nonempty α], ⋃ i, s i = Set.univ → Nonempty ι - Set.sigmaToiUnion Mathlib.Data.Set.Lattice
{α : Type u_1} → {β : Type u_2} → (t : α → Set β) → (i : α) × ↑(t i) → ↑(⋃ i, t i) - Set.iUnion_of_empty Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} [inst : IsEmpty ι] (s : ι → Set α), ⋃ i, s i = ∅ - Set.nonempty_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α}, (⋃ i, s i).Nonempty ↔ ∃ i, (s i).Nonempty - Set.iUnion_subset_iUnion_const Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : Set α}, (ι → ι₂) → ⋃ x, s ⊆ ⋃ x, s - Set.iUnion_singleton_eq_range Mathlib.Data.Set.Lattice
∀ {α : Type u_11} {β : Type u_12} (f : α → β), ⋃ x, {f x} = Set.range f - Set.range_eq_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_11} (f : ι → α), Set.range f = ⋃ i, {f i} - Set.iUnion_plift_down Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (f : ι → Set α), ⋃ i, f i.down = ⋃ i, f i - Set.iUnion_eq_if Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {p : Prop} [inst : Decidable p] (s : Set α), ⋃ (_ : p), s = if p then s else ∅ - Set.iUnion_plift_up Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (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_4} [inst : Nonempty ι] {f : ι → Set α} {s : Set α}, (∀ (i : ι), f i = s) → ⋃ i, f i = s - Set.sInter_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (s : ι → Set (Set α)), ⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i - Set.sUnion_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (s : ι → Set (Set α)), ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i - Set.iUnion_setOf Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (P : ι → α → Prop), ⋃ i, {x | P i x} = {x | ∃ i, P i x} - Set.iUnion_subset Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} {t : Set α}, (∀ (i : ι), s i ⊆ t) → ⋃ i, s i ⊆ t - Set.subset_iUnion_of_subset Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s : Set α} {t : ι → Set α} (i : ι), s ⊆ t i → s ⊆ ⋃ i, t i - Function.Surjective.iUnion_comp Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → ι₂}, 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_4} {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_4} {s : ι → Set α} {a : α} (i : ι), a ∈ s i → a ∈ ⋃ i, s i - Set.surjOn_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.SurjOn f s (t i)) → Set.SurjOn f s (⋃ i, t 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_4} (s : ι → Set β), (⋃ i, s i)ᶜ = ⋂ i, (s i)ᶜ - Set.iInter_eq_compl_iUnion_compl Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β), ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ - Set.iUnion_eq_compl_iInter_compl Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (s : ι → Set β), ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ - Set.iUnion_eq_univ_iff Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {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_4} (κ : ι → Sort u_11) (s : ι → Set α), ⋃ i, ⋃ x, s i ⊆ ⋃ i, s i - Set.mapsTo_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : Set β} {f : α → β}, Set.MapsTo f (⋃ i, s i) t ↔ ∀ (i : ι), Set.MapsTo f (s i) t - Set.iUnion_congr Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s t : ι → Set α}, (∀ (i : ι), s i = t i) → ⋃ i, s i = ⋃ i, t i - Set.iUnion_eq_dif Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {p : Prop} [inst : 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_4} {s : ι → Set α}, ⋃ i, s i = ∅ ↔ ∀ (i : ι), s i = ∅ - Set.iUnion_mono'' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → Set.iUnion s ⊆ Set.iUnion t - Set.image_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → Set α}, f '' ⋃ i, s i = ⋃ i, f '' s i - Set.preimage_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {s : ι → Set β}, f ⁻¹' ⋃ i, s i = ⋃ i, f ⁻¹' s i - Set.iUnion_comm Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} (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_11} (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_11} (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_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} (i : ι) (j : κ i), s i j ⊆ ⋃ i', ⋃ j', s i' j' - sSup_iUnion Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice β] (t : ι → Set β), sSup (⋃ i, t i) = ⨆ i, sSup (t i) - Set.iUnion_diff Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (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_4} {ι' : Sort u_5} {s : ι → ι' → Set α}, ⋃ j, ⋂ i, s i j ⊆ ⋂ i, ⋃ j, s i j - Set.iUnion_inter Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β), (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s - Set.inter_iUnion Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (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), (∀ (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_4} {s t : ι → Set α}, (∀ (i : ι), s i ⊆ t i) → ⋃ i, s i ⊆ ⋃ i, t i - Set.iUnion_prod' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α), ⋃ x, f x = ⋃ i, ⋃ j, f (i, j) - 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_4} [inst : 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_4} [inst : Nonempty ι] (s : Set β) (t : ι → Set β), (⋃ i, t i) ∪ s = ⋃ i, t i ∪ s - Set.mapsTo_iUnion_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.MapsTo f (s i) (t i)) → Set.MapsTo f (⋃ i, s i) (⋃ i, t i) - Set.surjOn_iUnion_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.SurjOn f (s i) (t i)) → Set.SurjOn f (⋃ i, s i) (⋃ i, t i) - Set.union_iUnion Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} [inst : Nonempty ι] (s : Set β) (t : ι → Set β), s ∪ ⋃ i, t i = ⋃ i, s ∪ 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_4} {p : ι → Prop} {f : Exists p → Set α}, ⋃ (x : Exists p), f x = ⋃ i, ⋃ (h : p i), f ⋯ - Set.iUnion_sigma Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_11} (s : Sigma γ → Set β), ⋃ ia, s ia = ⋃ i, ⋃ a, s ⟨i, a⟩ - Set.directedOn_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {r : α → α → Prop} {f : ι → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) f → (∀ (x : ι), DirectedOn r (f x)) → DirectedOn r (⋃ x, f x) - Set.directed_on_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {r : α → α → Prop} {f : ι → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) f → (∀ (x : ι), DirectedOn r (f x)) → DirectedOn r (⋃ x, f x) - Set.iUnion_congr_of_surjective Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {f : ι → Set α} {g : ι₂ → Set α} (h : ι → ι₂), Function.Surjective h → (∀ (x : ι), g (h x) = f x) → ⋃ x, f x = ⋃ y, g y - Set.iUnion_mono' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι₂ : Sort u_6} {s : ι → Set α} {t : ι₂ → Set α}, (∀ (i : ι), ∃ j, s i ⊆ t j) → ⋃ i, s i ⊆ ⋃ i, t i - Set.image2_iUnion_left Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : ι → Set α) (t : Set β), Set.image2 f (⋃ i, s i) t = ⋃ i, Set.image2 f (s i) t - Set.image2_iUnion_right Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} (f : α → β → γ) (s : Set α) (t : ι → Set β), Set.image2 f s (⋃ i, t i) = ⋃ i, Set.image2 f s (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.iUnion_iUnion_eq' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β}, ⋃ x, ⋃ y, ⋃ (_ : f y = x), g x = ⋃ y, g (f y) - Set.iUnion_union_distrib Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (s t : ι → Set β), ⋃ i, s i ∪ t i = (⋃ i, s i) ∪ ⋃ i, t i - Set.inj_on_iUnion_of_directed Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) s → ∀ {f : α → β}, (∀ (i : ι), Set.InjOn f (s i)) → Set.InjOn f (⋃ i, s i) - Set.sUnion_eq_biUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {s : Set (Set α)}, ⋃₀ s = ⋃ i ∈ s, i - Set.bijective_iff_bijective_of_iUnion_eq_univ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {U : ι → Set β}, Set.iUnion U = Set.univ → (Function.Bijective f ↔ ∀ (i : ι), Function.Bijective ((U i).restrictPreimage f)) - Set.iUnion_sigma' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : α → Type u_11} (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_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set α}, (∀ (i : ι) (j : κ i), s i j ⊆ t) → ⋃ i, ⋃ j, s i j ⊆ t - Set.injective_iff_injective_of_iUnion_eq_univ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {U : ι → Set β}, Set.iUnion U = Set.univ → (Function.Injective f ↔ ∀ (i : ι), Function.Injective ((U i).restrictPreimage f)) - Set.subset_iUnion₂_of_subset Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set α} (i : ι) (j : κ i), s ⊆ t i j → s ⊆ ⋃ i, ⋃ j, t i j - Set.surjective_iff_surjective_of_iUnion_eq_univ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : α → β} {U : ι → Set β}, Set.iUnion U = Set.univ → (Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f)) - 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_11} {α : Type u_12} {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_4} {κ : ι → Sort u_7} {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_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {a : α} {i : ι} (j : κ i), a ∈ s i j → a ∈ ⋃ i, ⋃ j, s i j - Set.surjOn_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set β} {f : α → β}, (∀ (i : ι) (j : κ i), Set.SurjOn f s (t i j)) → Set.SurjOn f s (⋃ i, ⋃ j, t 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.image_eq_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = ⋃ i ∈ s, {f i} - Set.mapsTo_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set β} {f : α → β}, Set.MapsTo f (⋃ i, ⋃ j, s i j) t ↔ ∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) t - Set.biUnion_empty Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ ∅, s x = ∅ - Set.bijOn_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.InjOn f (⋃ i, s i) → Set.BijOn f (⋃ i, s i) (⋃ i, t i) - 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_preimage_singleton Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s - 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_4} {κ : ι → Sort u_7} {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 : α}, x ∈ s → u x ⊆ ⋃ x ∈ s, u x - Set.biUnion_range Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {f : ι → α} {g : α → Set β}, ⋃ x ∈ Set.range f, g x = ⋃ y, g (f y) - Set.biUnion_range_preimage_singleton Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (f : α → β), ⋃ y ∈ Set.range f, f ⁻¹' {y} = Set.univ - Set.compl_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} (s : (i : ι) → κ i → Set α), (⋃ i, ⋃ j, s i j)ᶜ = ⋂ i, ⋂ j, (s i j)ᶜ - Set.iUnion_image_left Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β}, ⋃ a ∈ s, f a '' t = Set.image2 f s t - Set.iUnion_image_preimage_sigma_mk_eq_self Mathlib.Data.Set.Lattice
∀ {ι : Type u_11} {σ : ι → Type u_12} (s : Set (Sigma σ)), ⋃ i, Sigma.mk i '' (Sigma.mk i ⁻¹' s) = s - Set.image_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β) (s : (i : ι) → κ i → Set α), f '' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f '' s i j - Set.mem_iUnion₂ Mathlib.Data.Set.Lattice
∀ {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} {x : γ} {s : (i : ι) → κ i → Set γ}, x ∈ ⋃ i, ⋃ j, s i j ↔ ∃ i j, x ∈ s i j - Set.preimage_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {f : α → β} {s : (i : ι) → κ i → Set β}, f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j - Set.iUnion_image_right Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β}, ⋃ b ∈ t, (fun x => f x b) '' s = Set.image2 f s t - 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 - Set.bijOn_iUnion_of_directed Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) s → ∀ {t : ι → Set β} {f : α → β}, (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.BijOn f (⋃ i, s i) (⋃ i, t i) - Set.iUnion_univ_pi Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {π : α → Type u_11} {ι : α → Type u_12} (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_4} {κ : ι → Sort u_7} (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_4} {κ : ι → Sort u_7} (s : Set α) (t : (i : ι) → κ i → Set α), s ∩ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ∩ t i j - Set.iUnion_prod_const Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : ι → Set α} {t : Set β}, (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t - Set.iUnion_range_eq_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (C : ι → Set α) {f : (x : ι) → β → ↑(C x)}, (∀ (x : ι), Function.Surjective (f x)) → (⋃ y, Set.range fun x => ↑(f x y)) = ⋃ x, C x - Set.prod_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {s : Set α} {t : ι → Set β}, s ×ˢ ⋃ i, t i = ⋃ i, s ×ˢ t i - Set.iUnion₂_congr Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), s i j = t i j) → ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, t i j - Monotone.iUnion_nat_add Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {f : ℕ → Set α}, Monotone f → ∀ (k : ℕ), ⋃ n, f (n + k) = ⋃ n, f n - Set.iUnion_eq_range_psigma Mathlib.Data.Set.Lattice
∀ {β : Type u_2} {ι : Sort u_4} (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.image2_iUnion₂_left Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ) (s : (i : ι) → κ i → Set α) (t : Set β), Set.image2 f (⋃ i, ⋃ j, s i j) t = ⋃ i, ⋃ j, Set.image2 f (s i j) t - Set.image2_iUnion₂_right Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_4} {κ : ι → Sort u_7} (f : α → β → γ) (s : Set α) (t : (i : ι) → κ i → Set β), Set.image2 f s (⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, Set.image2 f s (t i j) - Set.mem_biUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : α → Set β} {x : α} {y : β}, x ∈ s → y ∈ t x → y ∈ ⋃ x ∈ s, t x - Set.iUnion_coe_set Mathlib.Data.Set.Lattice
∀ {α : Type u_11} {β : Type u_12} (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_4} {κ : ι → Sort u_7} {s t : (i : ι) → κ i → Set α}, (∀ (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.mapsTo_iUnion₂_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β}, (∀ (i : ι) (j : κ i), Set.MapsTo f (s i j) (t i j)) → Set.MapsTo f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j) - Set.surjOn_iUnion₂_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : (i : ι) → κ i → Set β} {f : α → β}, (∀ (i : ι) (j : κ i), Set.SurjOn f (s i j) (t i j)) → Set.SurjOn f (⋃ i, ⋃ j, s i j) (⋃ i, ⋃ j, t i j) - Set.iUnion_ite Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) [inst : 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.prod_eq_biUnion_left Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t - Set.prod_eq_biUnion_right Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ⋃ b ∈ t, (fun a => (a, b)) '' s - Set.sigmaToiUnion_bijective Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (t : α → Set β), (Pairwise fun i j => Disjoint (t i) (t j)) → Function.Bijective (Set.sigmaToiUnion t) - Set.sigmaToiUnion_injective Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} (t : α → Set β), (Pairwise fun i j => Disjoint (t i) (t j)) → Function.Injective (Set.sigmaToiUnion t) - Set.iUnion₂_comm Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {κ₁ : ι → Sort u_8} {κ₂ : ι → Sort u_9} (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 β}, s ⊆ s' → ⋃ x ∈ s, t x ⊆ ⋃ x ∈ s', t x - Set.biUnion_image Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set γ} {f : γ → α} {g : α → Set β}, ⋃ x ∈ f '' s, g x = ⋃ y ∈ s, g (f y) - Set.iUnion₂_mono' Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {κ : ι → Sort u_7} {κ' : ι' → Sort u_10} {s : (i : ι) → κ i → Set α} {t : (i' : ι') → κ' i' → Set α}, (∀ (i : ι) (j : κ i), ∃ i' j', s i j ⊆ t i' j') → ⋃ i, ⋃ j, s i j ⊆ ⋃ i', ⋃ j', t i' j' - Set.iUnion_prod Mathlib.Data.Set.Lattice
∀ {ι : Type u_11} {ι' : Type u_12} {α : Type u_13} {β : Type u_14} (s : ι → Set α) (t : ι' → Set β), ⋃ x, s x.1 ×ˢ t x.2 = (⋃ i, s i) ×ˢ ⋃ i, t i - Set.iUnion₂_prod_const Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : (i : ι) → κ i → Set α} {t : Set β}, (⋃ i, ⋃ j, s i j) ×ˢ t = ⋃ i, ⋃ j, s i j ×ˢ t - Set.image2_eq_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (s : Set α) (t : Set β), Set.image2 f s t = ⋃ i ∈ s, ⋃ j ∈ t, {f i j} - Set.prod_iUnion₂ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set β}, s ×ˢ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s ×ˢ t i j - Set.biInter_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} (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_4} (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_4} (p : ι → Prop) [inst : 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_4} {ι' : Sort u_5} (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_4} {ι' : Sort u_5} (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_11} {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_11} {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 β}, s' ⊆ s → (∀ x ∈ s, t x ⊆ t' x) → ⋃ x ∈ s', t x ⊆ ⋃ x ∈ s, t' x - iInf_iUnion Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : 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_4} [inst : CompleteLattice β] (s : ι → Set α) (f : α → β), ⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a - Set.iUnion_inter_of_monotone Mathlib.Data.Set.Lattice
∀ {ι : Type u_11} {α : Type u_12} [inst : Preorder ι] [inst_1 : IsDirected ι fun x1 x2 => x1 ≤ x2] {s t : ι → Set α}, Monotone s → Monotone t → ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i - Set.disjoint_iUnion₂_left Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_7} {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_4} {κ : ι → Sort u_7} {s : Set α} {t : (i : ι) → κ i → Set α}, Disjoint s (⋃ i, ⋃ j, t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j) - Set.iUnion_inter_of_antitone Mathlib.Data.Set.Lattice
∀ {ι : Type u_11} {α : Type u_12} [inst : Preorder ι] [inst_1 : IsDirected ι (Function.swap fun x1 x2 => x1 ≤ x2)] {s t : ι → Set α}, Antitone s → Antitone t → ⋃ i, s i ∩ t i = (⋃ i, s i) ∩ ⋃ i, t i - 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.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_11} {β : Type u_12} (C : Set (Set α)) {f : (s : ↑C) → β → ↑↑s}, (∀ (s : ↑C), Function.Surjective (f s)) → (⋃ y, Set.range fun s => ↑(f s y)) = ⋃₀ C - Set.iUnion_prod_of_monotone Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : SemilatticeSup α] {s : α → Set β} {t : α → Set γ}, Monotone s → Monotone t → ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x - Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ Mathlib.Data.Set.Lattice
∀ {α : Type u_1} {ι : Type u_11} {Es : ι → Set α}, ⋃ i, Es i = Set.univ → (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} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α), sInf (⋃ i, Set.Ici (f i)) = ⨅ i, f i - sSup_iUnion_Iic Mathlib.Order.ConditionallyCompleteLattice.Basic
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] (f : ι → α), sSup (⋃ i, Set.Iic (f i)) = ⨆ i, f i - Set.iUnion_inv Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Inv α] (s : ι → Set α), (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹ - Set.iUnion_neg Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Neg α] (s : ι → Set α), -⋃ i, s i = ⋃ i, -s i - Set.add_iUnion Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : Set α) (t : ι → Set α), s + ⋃ i, t i = ⋃ i, s + t i - Set.div_iUnion Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : Set α) (t : ι → Set α), s / ⋃ i, t i = ⋃ i, s / t i - Set.iUnion_add Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Add α] (s : ι → Set α) (t : Set α), (⋃ i, s i) + t = ⋃ i, s i + t - Set.iUnion_div Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Div α] (s : ι → Set α) (t : Set α), (⋃ i, s i) / t = ⋃ i, s i / t - Set.iUnion_mul Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : ι → Set α) (t : Set α), (⋃ i, s i) * t = ⋃ i, s i * t - Set.iUnion_sub Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : ι → Set α) (t : Set α), (⋃ i, s i) - t = ⋃ i, s i - t - Set.mul_iUnion Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : Set α) (t : ι → Set α), s * ⋃ i, t i = ⋃ i, s * t i - Set.sub_iUnion Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : Set α) (t : ι → Set α), s - ⋃ i, t i = ⋃ i, s - t i - Set.iUnion_add_left_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Add α] {s t : Set α}, ⋃ a ∈ s, (fun x => a + x) '' t = s + t - Set.iUnion_add_right_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Add α] {s t : Set α}, ⋃ a ∈ t, (fun x => x + a) '' s = s + t - Set.iUnion_div_left_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Div α] {s t : Set α}, ⋃ a ∈ s, (fun x => a / x) '' t = s / t - Set.iUnion_div_right_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Div α] {s t : Set α}, ⋃ a ∈ t, (fun x => x / a) '' s = s / t - Set.iUnion_mul_left_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, ⋃ a ∈ s, (fun x => a * x) '' t = s * t - Set.iUnion_mul_right_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, ⋃ a ∈ t, (fun x => x * a) '' s = s * t - Set.iUnion_sub_left_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, ⋃ a ∈ s, (fun x => a - x) '' t = s - t - Set.iUnion_sub_right_image Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, ⋃ a ∈ t, (fun x => x - a) '' s = s - t - Set.add_iUnion₂ Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : Set α) (t : (i : ι) → κ i → Set α), s + ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s + t i j - Set.div_iUnion₂ Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : Set α) (t : (i : ι) → κ i → Set α), s / ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s / t i j - Set.iUnion₂_add Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : (i : ι) → κ i → Set α) (t : Set α), (⋃ i, ⋃ j, s i j) + t = ⋃ i, ⋃ j, s i j + t - Set.iUnion₂_div Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : (i : ι) → κ i → Set α) (t : Set α), (⋃ i, ⋃ j, s i j) / t = ⋃ i, ⋃ j, s i j / t - Set.iUnion₂_mul Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : (i : ι) → κ i → Set α) (t : Set α), (⋃ i, ⋃ j, s i j) * t = ⋃ i, ⋃ j, s i j * t - Set.iUnion₂_sub Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Sub α] (s : (i : ι) → κ i → Set α) (t : Set α), (⋃ i, ⋃ j, s i j) - t = ⋃ i, ⋃ j, s i j - t - Set.mul_iUnion₂ Mathlib.Algebra.Group.Pointwise.Set
∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : Set α) (t : (i : ι) → κ i → Set α), s * ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s * t i j
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try 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 findtsum_lt_tsum
even though the hypothesisf 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, _ * _, _ ^ _, |- _ < _ → _
woould 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 7eaed1d
serving mathlib revision 329f679