Loogle!
Result
Found 63 definitions mentioning BoxIntegral.Prepartition.iUnion.
- BoxIntegral.Prepartition.iUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
{ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.Prepartition I → Set (ι → ℝ) - BoxIntegral.Prepartition.iUnion_subset Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion ⊆ ↑I - BoxIntegral.Prepartition.IsPartition.iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition → π.iUnion = ↑I - BoxIntegral.Prepartition.isPartition_iff_iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition ↔ π.iUnion = ↑I - BoxIntegral.Prepartition.iUnion_single Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (h : J ≤ I), (BoxIntegral.Prepartition.single I J h).iUnion = ↑J - BoxIntegral.Prepartition.iUnion_top Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊤.iUnion = ↑I - BoxIntegral.Prepartition.IsPartition.iUnion_subset Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition → ∀ (π₁ : BoxIntegral.Prepartition I), π₁.iUnion ⊆ π.iUnion - BoxIntegral.Prepartition.iUnion_bot Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊥.iUnion = ∅ - BoxIntegral.Prepartition.iUnion_mono Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁ ≤ π₂ → π₁.iUnion ⊆ π₂.iUnion - BoxIntegral.Prepartition.subset_iUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → ↑J ⊆ π.iUnion - BoxIntegral.Prepartition.iUnion_restrict Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), (π.restrict J).iUnion = ↑J ∩ π.iUnion - BoxIntegral.Prepartition.iUnion_inf Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I), (π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion - BoxIntegral.Prepartition.iUnion_eq_empty Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.Prepartition I}, π₁.iUnion = ∅ ↔ π₁ = ⊥ - BoxIntegral.Prepartition.iUnion_filter_not Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (p : BoxIntegral.Box ι → Prop), (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion - BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.boxes ⊆ π₂.boxes → π₂.iUnion ⊆ π₁.iUnion → π₁ = π₂ - BoxIntegral.Prepartition.iUnion_biUnion_partition Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, (∀ J ∈ π, (πi J).IsPartition) → (π.biUnion πi).iUnion = π.iUnion - BoxIntegral.Prepartition.iUnion_def Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π, ↑J - BoxIntegral.Prepartition.mem_iUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ}, x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J - BoxIntegral.Prepartition.iUnion.eq_1 Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π, ↑J - BoxIntegral.Prepartition.iUnion_def' Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π.boxes, ↑J - BoxIntegral.Prepartition.iUnion_biUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion - BoxIntegral.Prepartition.disjUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
{ι : Type u_1} → {I : BoxIntegral.Box ι} → (π₁ π₂ : BoxIntegral.Prepartition I) → Disjoint π₁.iUnion π₂.iUnion → BoxIntegral.Prepartition I - BoxIntegral.Prepartition.disjoint_boxes_of_disjoint_iUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, Disjoint π₁.iUnion π₂.iUnion → Disjoint π₁.boxes π₂.boxes - BoxIntegral.Prepartition.le_iff_nonempty_imp_le_and_iUnion_subset Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I}, π₁ ≤ π₂ ↔ (∀ J ∈ π₁, ∀ J' ∈ π₂, (↑J ∩ ↑J').Nonempty → J ≤ J') ∧ π₁.iUnion ⊆ π₂.iUnion - BoxIntegral.Prepartition.iUnion_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion - BoxIntegral.Prepartition.distortion_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} [inst : Fintype ι] (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion - BoxIntegral.Prepartition.disjUnion_boxes Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes - BoxIntegral.Prepartition.mem_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (H : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₁.disjUnion π₂ H ↔ J ∈ π₁ ∨ J ∈ π₂ - BoxIntegral.Prepartition.disjUnion.eq_1 Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion), π₁.disjUnion π₂ h = { boxes := π₁.boxes ∪ π₂.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ } - BoxIntegral.Prepartition.iUnion_ofWithBot Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (WithBot (BoxIntegral.Box ι))) (le_of_mem : ∀ J ∈ boxes, J ≤ ↑I) (pairwise_disjoint : (↑boxes).Pairwise Disjoint), (BoxIntegral.Prepartition.ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J - BoxIntegral.Prepartition.sum_disj_union_boxes Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} {M : Type u_2} [inst : AddCommMonoid M], Disjoint π₁.iUnion π₂.iUnion → ∀ (f : BoxIntegral.Box ι → M), ∑ J ∈ π₁.boxes ∪ π₂.boxes, f J = ∑ J ∈ π₁.boxes, f J + ∑ J ∈ π₂.boxes, f J - BoxIntegral.Prepartition.isPartitionDisjUnionOfEqDiff Mathlib.Analysis.BoxIntegral.Partition.Basic
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (h : π₂.iUnion = ↑I \ π₁.iUnion), (π₁.disjUnion π₂ ⋯).IsPartition - BoxIntegral.TaggedPrepartition.iUnion_toPrepartition Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion = π.iUnion - BoxIntegral.TaggedPrepartition.iUnion_mk Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → ι → ℝ) (h : ∀ (J : BoxIntegral.Box ι), f J ∈ BoxIntegral.Box.Icc I), { toPrepartition := π, tag := f, tag_mem_Icc := h }.iUnion = π.iUnion - BoxIntegral.Prepartition.iUnion_toSubordinate Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π.toSubordinate r).iUnion = π.iUnion - BoxIntegral.TaggedPrepartition.unionComplToSubordinate Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
{ι : Type u_1} → [inst : Fintype ι] → {I : BoxIntegral.Box ι} → (π₁ : BoxIntegral.TaggedPrepartition I) → (π₂ : BoxIntegral.Prepartition I) → π₂.iUnion = ↑I \ π₁.iUnion → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I - BoxIntegral.TaggedPrepartition.isPartition_unionComplToSubordinate Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π₁.unionComplToSubordinate π₂ hU r).IsPartition - BoxIntegral.TaggedPrepartition.iUnion_unionComplToSubordinate_boxes Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π₁.unionComplToSubordinate π₂ hU r).iUnion = ↑I - BoxIntegral.TaggedPrepartition.distortion_unionComplToSubordinate Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π₁.unionComplToSubordinate π₂ hU r).distortion = max π₁.distortion π₂.distortion - BoxIntegral.TaggedPrepartition.unionComplToSubordinate.eq_1 Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)), π₁.unionComplToSubordinate π₂ hU r = π₁.disjUnion (π₂.toSubordinate r) ⋯ - BoxIntegral.Prepartition.exists_tagged_le_isHenstock_isSubordinate_iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (r : (ι → ℝ) → ↑(Set.Ioi 0)) (π : BoxIntegral.Prepartition I), ∃ π', π'.toPrepartition ≤ π ∧ π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion - BoxIntegral.TaggedPrepartition.unionComplToSubordinate_boxes Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} (π₁ : BoxIntegral.TaggedPrepartition I) (π₂ : BoxIntegral.Prepartition I) (hU : π₂.iUnion = ↑I \ π₁.iUnion) (r : (ι → ℝ) → ↑(Set.Ioi 0)), (π₁.unionComplToSubordinate π₂ hU r).boxes = π₁.boxes ∪ (π₂.toSubordinate r).boxes - BoxIntegral.Prepartition.iUnion_split Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ), (BoxIntegral.Prepartition.split I i x).iUnion = ↑I - BoxIntegral.Prepartition.iUnion_splitMany Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)), (BoxIntegral.Prepartition.splitMany I s).iUnion = ↑I - BoxIntegral.Prepartition.iUnion_compl Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I), π.compl.iUnion = ↑I \ π.iUnion - BoxIntegral.Prepartition.compl_congr Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.iUnion = π₂.iUnion → π₁.compl = π₂.compl - BoxIntegral.Prepartition.exists_iUnion_eq_diff Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I), ∃ π', π'.iUnion = ↑I \ π.iUnion - BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filter Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I), ∀ᶠ (t : Finset (ι × ℝ)) in Filter.atTop, π ⊓ BoxIntegral.Prepartition.splitMany I t = (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion - BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite Mathlib.Analysis.BoxIntegral.Partition.Split
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (s : Set (BoxIntegral.Prepartition I)), s.Finite → ∃ t, ∀ π ∈ s, π ⊓ BoxIntegral.Prepartition.splitMany I t = (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion - BoxIntegral.IntegrationParams.toFilteriUnion_congr Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams) {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.iUnion = π₂.iUnion → BoxIntegral.IntegrationParams.toFilteriUnion I π₁ = BoxIntegral.IntegrationParams.toFilteriUnion I π₂ - BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I), l.toFilter I ⊓ Filter.principal {π | π.iUnion = π₀.iUnion} = BoxIntegral.IntegrationParams.toFilteriUnion I π₀ - BoxIntegral.IntegrationParams.toFilterDistortioniUnion.eq_1 Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal) (π₀ : BoxIntegral.Prepartition I), l.toFilterDistortioniUnion I c π₀ = l.toFilterDistortion I c ⊓ Filter.principal {π | π.iUnion = π₀.iUnion} - BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal) (π₀ : BoxIntegral.Prepartition I), (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun r => {π | l.MemBaseSet I c r π ∧ π.iUnion = π₀.iUnion} - BoxIntegral.IntegrationParams.MemBaseSet.exists_compl Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I}, l.MemBaseSet I c r π → l.bDistortion = true → ∃ π', π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c - BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I), (BoxIntegral.IntegrationParams.toFilteriUnion I π₀).HasBasis (fun r => ∀ (c : NNReal), l.RCond (r c)) fun r => {π | ∃ c, l.MemBaseSet I c (r c) π ∧ π.iUnion = π₀.iUnion} - BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} (l : BoxIntegral.IntegrationParams) (π₀ : BoxIntegral.Prepartition I), π₀.distortion ≤ c → π₀.compl.distortion ≤ c → ∀ (r : (ι → ℝ) → ↑(Set.Ioi 0)), ∃ π, l.MemBaseSet I c r π ∧ π.toPrepartition ≤ π₀ ∧ π.iUnion = π₀.iUnion - BoxIntegral.IntegrationParams.MemBaseSet.mk Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι → ℝ) → ↑(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I}, π.IsSubordinate r → (l.bHenstock = true → π.IsHenstock) → (l.bDistortion = true → π.distortion ≤ c) → (l.bDistortion = true → ∃ π', π'.iUnion = ↑I \ π.iUnion ∧ π'.distortion ≤ c) → l.MemBaseSet I c r π - BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c₁ c₂ : NNReal} {l : BoxIntegral.IntegrationParams} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π₁ π₂ : BoxIntegral.TaggedPrepartition I}, l.MemBaseSet I c₁ r₁ π₁ → l.MemBaseSet I c₂ r₂ π₂ → π₁.iUnion = π₂.iUnion → ∃ π, π.iUnion = ↑I \ π₁.iUnion ∧ (l.bDistortion = true → π.distortion ≤ c₁) ∧ (l.bDistortion = true → π.distortion ≤ c₂) - BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate Mathlib.Analysis.BoxIntegral.Partition.Filter
∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {l : BoxIntegral.IntegrationParams} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π₁ : BoxIntegral.TaggedPrepartition I}, l.MemBaseSet I c r₁ π₁ → (∀ x ∈ BoxIntegral.Box.Icc I, r₂ x ≤ r₁ x) → ∀ {π₂ : BoxIntegral.Prepartition I} (hU : π₂.iUnion = ↑I \ π₁.iUnion), (l.bDistortion = true → π₂.distortion ≤ c) → l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂) - BoxIntegral.BoxAdditiveMap.sum_boxes_congr Mathlib.Analysis.BoxIntegral.Partition.Additive
∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι} [inst_1 : Finite ι] (f : BoxIntegral.BoxAdditiveMap ι M I₀), ↑I ≤ I₀ → ∀ {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.iUnion = π₂.iUnion → ∑ J ∈ π₁.boxes, f J = ∑ J ∈ π₂.boxes, f J - BoxIntegral.Prepartition.measure_iUnion_toReal Mathlib.Analysis.BoxIntegral.Partition.Measure
∀ {ι : Type u_1} [inst : Finite ι] {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (μ : MeasureTheory.Measure (ι → ℝ)) [inst : MeasureTheory.IsLocallyFiniteMeasure μ], (μ π.iUnion).toReal = ∑ J ∈ π.boxes, (μ ↑J).toReal - BoxIntegral.Integrable.sum_integral_congr Mathlib.Analysis.BoxIntegral.Basic
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} [inst_5 : CompleteSpace F], BoxIntegral.Integrable I l f vol → ∀ {π₁ π₂ : BoxIntegral.Prepartition I}, π₁.iUnion = π₂.iUnion → ∑ J ∈ π₁.boxes, BoxIntegral.integral J l f vol = ∑ J ∈ π₂.boxes, BoxIntegral.integral J l f vol - BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq Mathlib.Analysis.BoxIntegral.Basic
∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [inst_4 : Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : NNReal} {ε : ℝ} [inst_5 : CompleteSpace F] (h : BoxIntegral.Integrable I l f vol), 0 < ε → l.MemBaseSet I c (h.convergenceR ε c) π → ∀ {π₀ : BoxIntegral.Prepartition I}, π.iUnion = π₀.iUnion → dist (BoxIntegral.integralSum f vol π) (∑ J ∈ π₀.boxes, BoxIntegral.integral J l f vol) ≤ ε
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 2a811d0