Loogle!
Result
Found 41 definitions mentioning BoxIntegral.TaggedPrepartition.iUnion.
- BoxIntegral.TaggedPrepartition.iUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
{ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → Set (ι → ℝ) - BoxIntegral.TaggedPrepartition.iUnion_subset Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion ⊆ ↑I - BoxIntegral.TaggedPrepartition.iUnion_toPrepartition Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion = π.iUnion - BoxIntegral.TaggedPrepartition.isPartition_iff_iUnion_eq Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.IsPartition ↔ π.iUnion = ↑I - BoxIntegral.TaggedPrepartition.subset_iUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), J ∈ π → ↑J ⊆ π.iUnion - BoxIntegral.TaggedPrepartition.iUnion_filter_not Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop), (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion - BoxIntegral.TaggedPrepartition.iUnion_def Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I), π.iUnion = ⋃ J ∈ π, ↑J - BoxIntegral.TaggedPrepartition.mem_iUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) {x : ι → ℝ}, x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J - BoxIntegral.Prepartition.iUnion_biUnionTagged Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J), (π.biUnionTagged πi).iUnion = ⋃ J ∈ π, (πi J).iUnion - BoxIntegral.TaggedPrepartition.disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
{ι : Type u_1} → {I : BoxIntegral.Box ι} → (π₁ π₂ : BoxIntegral.TaggedPrepartition I) → Disjoint π₁.iUnion π₂.iUnion → BoxIntegral.TaggedPrepartition I - BoxIntegral.TaggedPrepartition.IsHenstock.disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I}, π₁.IsHenstock → π₂.IsHenstock → ∀ (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).IsHenstock - BoxIntegral.TaggedPrepartition.iUnion_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion - BoxIntegral.TaggedPrepartition.distortion_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} [inst : Fintype ι] (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).distortion = max π₁.distortion π₂.distortion - BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₁ → (π₁.disjUnion π₂ h).tag J = π₁.tag J - BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_right Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₂ → (π₁.disjUnion π₂ h).tag J = π₂.tag J - 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.TaggedPrepartition.iUnion_single Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I), (BoxIntegral.TaggedPrepartition.single I J hJ x h).iUnion = ↑J - BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)} [inst : Fintype ι], π₁.IsSubordinate r → π₂.IsSubordinate r → ∀ (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).IsSubordinate r - BoxIntegral.TaggedPrepartition.mem_disjUnion Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₁.disjUnion π₂ h ↔ J ∈ π₁ ∨ J ∈ π₂ - BoxIntegral.TaggedPrepartition.disjUnion_boxes Mathlib.Analysis.BoxIntegral.Partition.Tagged
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).boxes = π₁.boxes ∪ π₂.boxes - 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.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.integralSum_disjUnion 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 ι} (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion), BoxIntegral.integralSum f vol (π₁.disjUnion π₂ h) = BoxIntegral.integralSum f vol π₁ + BoxIntegral.integralSum 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) ≤ ε - BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet 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) ⊤} {c₁ c₂ : NNReal} {ε₁ ε₂ : ℝ} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.Integrable I l f vol), 0 < ε₁ → 0 < ε₂ → l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁ → l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂ → π₁.iUnion = π₂.iUnion → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε₁ + ε₂ - BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity 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) ⊤}, BoxIntegral.Integrable I l f vol → Filter.Tendsto (fun π => (BoxIntegral.integralSum f vol π.1, BoxIntegral.integralSum f vol π.2)) (l.toFilter I ×ˢ l.toFilter I ⊓ Filter.principal {π | π.1.iUnion = π.2.iUnion}) (uniformity F)
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