BoxIntegral.Prepartition.isPartitionTop
theorem BoxIntegral.Prepartition.isPartitionTop : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ⊤.IsPartition
The theorem `BoxIntegral.Prepartition.isPartitionTop` states that for any type `ι` and any box `I` of type `BoxIntegral.Box ι`, the top element `⊤` of the prepartitions of `I` is a partition. This implies that the entirety of the box `I` is covered by the boxes of the top element prepartition.
More concisely: The top element of the prepartitions of a box integral over type `ι` is a partition, covering the entire box.
|
BoxIntegral.Prepartition.card_filter_mem_Icc_le
theorem BoxIntegral.Prepartition.card_filter_mem_Icc_le :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [inst : Fintype ι] (x : ι → ℝ),
(Finset.filter (fun J => x ∈ BoxIntegral.Box.Icc J) π.boxes).card ≤ 2 ^ Fintype.card ι
This theorem states that for any prepartition `π` of a box `I` in a finite-dimensional space `ι`, and for any point `x` given as a real-valued function on `ι`, the number of boxes in `π` that contain `x` in their closure is at most `2 ^ Fintype.card ι`. Here, `Fintype.card ι` represents the number of elements in `ι`, which is finite by assumption, so `2 ^ Fintype.card ι` gives the maximum possible number of boxes. The closure of a box is represented by `BoxIntegral.Box.Icc J` where `J` is a box in the prepartition. The theorem essentially counts the boxes containing `x` in their closure and asserts this number is bounded above by `2 ^ Fintype.card ι`.
More concisely: For any prepartition of a finite-dimensional space and real-valued function, the number of boxes in the prepartition containing the function value in their closure is bounded above by 2 raised to the power of the number of elements in the space.
|
Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.1
theorem Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.1 :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), (J ∈ π.boxes) = (J ∈ π)
This theorem states that for any type `ι`, any given boxes `I` and `J`, and any prepartition `π` of `I`, the condition of `J` being in the set of boxes of `π` is equivalent to `J` being in `π`. In other words, for any box `J` and prepartition `π`, `J` is a part of `π` if and only if `J` is among the boxes that make up `π`.
More concisely: For any type `ι`, prepartition `π` of `ι`, and box `J`, `J ∈ π` if and only if `J = some box in π`.
|
BoxIntegral.Prepartition.mem_restrict
theorem BoxIntegral.Prepartition.mem_restrict :
∀ {ι : Type u_1} {I J J₁ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'
The theorem `BoxIntegral.Prepartition.mem_restrict` states that for any type `ι`, and any three boxes `I`, `J`, and `J₁` of type `ι`, along with a prepartition `π` of box `I`, a box `J₁` is in the restricted prepartition of `π` to box `J` if and only if there exists a box `J'` in `π` such that the intersection of the boxes `J` and `J'` (in the underlying set) is equal to the underlying set of box `J₁`.
More concisely: For any type ι, box I, prepartition π of I, and boxes J, J₁, J is in the restricted prepartition of π to J if and only if there exists a box J' in π such that J ∩ J' = J₁.
|
BoxIntegral.Prepartition.mem_biUnion
theorem BoxIntegral.Prepartition.mem_biUnion :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
{πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi ↔ ∃ J' ∈ π, J ∈ πi J'
This theorem states that, for any type `ι`, any boxes `I` and `J`, a partition `π` of `I`, and a function `πi` that associates each box `J` to a partition of `J`, the box `J` belongs to the biUnion of `π` and `πi` if and only if there exists a box `J'` in `π` such that `J` belongs to the partition `πi J'`.
In more detail, the `BoxIntegral.Prepartition.biUnion` operation takes a partition of a box and a function that gives a partition for every box, and combines them into a single partition. The theorem then characterizes membership in this combined partition.
More concisely: For any type `ι`, given a partition `π` of a box `I` and a function `πi` that maps each box `J` to a partition of `J`, a box `J` belongs to the biUnion of `π` and `πi` if and only if there exists a box `J'` in `π` such that `J` is in the partition `πi(J')`.
|
BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq
theorem BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (x : ι → ℝ),
Set.InjOn (fun J => {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ BoxIntegral.Box.Icc J}
This theorem is an auxiliary lemma used in the proof of the assertion that a given point cannot belong to more than `2 ^ Fintype.card ι` closed boxes of a prepartition. The theorem states that, for any type `ι`, any integral box `I` of type `ι`, any prepartition `π` of `I`, and any real-valued function `x` on `ι`, the function mapping each box `J` to the set of indices `i` for which the lower bound of `J` at `i` equals `x(i)`, is injective when restricted to the set of boxes `J` that are in `π` and contain `x` in their closed version. In other words, no two boxes in the prepartition that contain `x` can have the exact same set of indices where their lower bound equals `x(i)`.
More concisely: For any type `ι`, prepartition `π` of an integral box `I` of type `ι`, and real-valued function `x` on `ι`, the function mapping each `J` in `π` containing `x` to the indices `i` in `J` with lower bound `x(i)` is injective.
|
Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.15
theorem Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.15 :
∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ ↑s) = (a ∈ s)
This theorem, named `_auxLemma.15` in the `Mathlib.Analysis.BoxIntegral.Partition.Basic` module, states that for all types `α`, for all `a` of type `α`, and for all finite sets `s` of type `α`, `a` is an element of the set `s` coerced to a set (`↑s`) if and only if `a` is an element of the set `s`. The coercion here refers to the type conversion from `Finset α` (finite set) to `Set α` in Lean 4.
More concisely: For any type `α`, element `a` of `α`, and finite set `s` of type `α`, `a` is in the set `s` if and only if `a` is in the set `↑s`. (Here, `↑s` denotes the set `{x : α | x ∈ s}`.)
|
BoxIntegral.Prepartition.disjoint_coe_of_mem
theorem BoxIntegral.Prepartition.disjoint_coe_of_mem :
∀ {ι : Type u_1} {I J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
J₁ ∈ π → J₂ ∈ π → J₁ ≠ J₂ → Disjoint ↑J₁ ↑J₂
This theorem states that for any type `ι`, and any three boxes `I`, `J1`, and `J2` in the Euclidean space of dimension `ι`, if we have a prepartition `π` of the box `I`, and if `J1` and `J2` are elements of this prepartition and are distinct, then `J1` and `J2` are disjoint. In other words, the intersection of `J1` and `J2` is the bottom element of the lattice (the empty set, in the context of sets of points in Euclidean space).
More concisely: Given a prepartition `π` of a box `I` in Euclidean space of dimension `ι`, if `J1` and `J2` are distinct elements of `π`, then `J1 ∩ J2` is the empty set.
|
Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.16
theorem Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.16 :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
{πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, (J ∈ π.biUnion πi) = ∃ J' ∈ π, J ∈ πi J'
This theorem from the `Mathlib.Analysis.BoxIntegral.Partition.Basic` in Lean 4 is about the union of a pre-partition of a box in n-dimensional space. Specifically, it states that for any types `ι`, any boxes `I` and `J`, a pre-partition `π` of box `I`, and a function `πi` that assigns a pre-partition to every box, then `J` is in the bi-union of the pre-partition `π` and the function `πi` if and only if there exists a box `J'` in the pre-partition `π` such that `J` is in the pre-partition `πi` assigned to `J'`.
More concisely: A box J is in the bi-union of a pre-partition π and the function πi if and only if there exists a box J' in π such that J is in the pre-partition πi assigned to J'.
|
BoxIntegral.Prepartition.biUnionIndex_mem
theorem BoxIntegral.Prepartition.biUnionIndex_mem :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
{πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J}, J ∈ π.biUnion πi → π.biUnionIndex πi J ∈ π
This theorem states that for any type `ι`, any boxes `I` and `J` of type `ι`, any prepartition `π` of the box `I`, and any function `πi` that associates to each box `J` a prepartition of `J`, if the box `J` is in the bi-union of `π` and `πi`, then the box returned by the function `biUnionIndex` applied to `π`, `πi`, and `J` is in the prepartition `π`.
More concisely: If `π` is a prepartition of type `ι`, `J` is a box of type `ι`, and `J` is in the bi-union of `π` and the image of `πi` on `J`, then the index of `J` in the bi-union `π ⋃ (π i)` is in the prepartition `π`.
|
BoxIntegral.Prepartition.iUnion_disjUnion
theorem BoxIntegral.Prepartition.iUnion_disjUnion :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I} (h : Disjoint π₁.iUnion π₂.iUnion),
(π₁.disjUnion π₂ h).iUnion = π₁.iUnion ∪ π₂.iUnion
This theorem states that for any given type `ι`, and any box `I` of this type, given two prepartitions `π₁` and `π₂` of this box which are disjoint (meaning their intersection is the bottom element in the lattice), the union of the two prepartitions is equal to the union of the individual sets covered by `π₁` and `π₂`. This essentially demonstrates that the operation of "disjoint union" on prepartitions coincides with the usual set theoretic union operation when applied to the sets they cover.
More concisely: For any type `ι` and disjoint partitions `π₁` and `π₂` of a box `I` of type `ι`, the union of `π₁ ⊎ π₂` equal the union of `π₁` and `π₂` as sets.
|
BoxIntegral.Prepartition.le_of_mem
theorem BoxIntegral.Prepartition.le_of_mem :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J ∈ π → J ≤ I
This theorem states that for any type `ι`, and any `I` and `J` that are boxes in `ι` (i.e., multidimensional intervals), if `π` is a prepartition of box `I` and box `J` is a member of this prepartition, then `J` is a subbox of `I`. In other words, every box in a prepartition of a given box is contained within that given box.
More concisely: For any type `ι`, and for any prepartition `π` of boxes in `ι`, if box `J` is an element of `π` and `I` is the box containing `J`, then `J` is a subbox of `I`.
|
BoxIntegral.Prepartition.injective_boxes
theorem BoxIntegral.Prepartition.injective_boxes :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, Function.Injective BoxIntegral.Prepartition.boxes
This theorem states that for any type `ι` and for any `BoxIntegral.Box` of that type `ι`, the `boxes` function of `BoxIntegral.Prepartition` is injective. This means that if we have two different prepartitions of the box `I`, the sets of boxes that they partition `I` into are also different. In other words, if the `boxes` function gives the same output for two prepartitions, then those prepartitions must have been the same to begin with. This is a property of the `boxes` function, which retrieves the set of boxes from a prepartition.
More concisely: For any type `ι` and `BoxIntegral.Box` of that type, the `boxes` function of `BoxIntegral.Prepartition` is an injection.
|
BoxIntegral.Prepartition.iUnion_biUnion
theorem BoxIntegral.Prepartition.iUnion_biUnion :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
(πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J), (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion
The theorem `BoxIntegral.Prepartition.iUnion_biUnion` states that for any type `ι`, given a box `I` of type `BoxIntegral.Box ι`, a prepartition `π` of `I`, and a function `πi` that returns a prepartition for each box `J` of type `BoxIntegral.Box ι`, the union of the boxes of the prepartition obtained by bisecting `π` using `πi` (`BoxIntegral.Prepartition.biUnion π πi`) is equal to the union of the unions of the boxes of the prepartitions returned by `πi` for each box `J` in `π`. In other words, bisecting the prepartition and then taking the union gives the same result as taking the union of the prepartitions for each box first and then taking the union.
More concisely: For any type ι, given a box I of type BoxIntegral.Box ι, a prepartition π of I, and a function πi that returns a prepartition for each box J of type BoxIntegral.Box ι, the union of the boxes in BoxIntegral.Prepartition.biUnion π πi equals the union of the unions of the boxes in the prepartitions returned by πi for each J in π.
|
Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.2
theorem Mathlib.Analysis.BoxIntegral.Partition.Basic._auxLemma.2 :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {s : Finset (BoxIntegral.Box ι)} {h₁ : ∀ J ∈ s, J ≤ I}
{h₂ : (↑s).Pairwise (Disjoint on BoxIntegral.Box.toSet)},
(J ∈ { boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ }) = (J ∈ s)
This theorem states that for all types `ι`, given two boxes `I` and `J` of type `ι`, and a finite set `s` of such boxes, with the condition that every box `J` in `s` is less than or equal to `I` and all boxes in the set `s` are pairwise disjoint (i.e., the intersection of any two distinct boxes is the bottom element), then a box `J` is in the set `{ boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ }` if and only if `J` is in the set `s`. This essentially says the set `{ boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ }` is equivalent to the set `s` in terms of its membership.
More concisely: Given a type `ι` and a finite set `s` of pairwise disjoint boxes `I` and `J` of type `ι` with `J ≤ I` for all `J` in `s`, the sets `{ boxes := s, le_of_mem' := h₁, pairwiseDisjoint := h₂ }` and `s` have equivalent membership.
|
BoxIntegral.Prepartition.eq_of_le_of_le
theorem BoxIntegral.Prepartition.eq_of_le_of_le :
∀ {ι : Type u_1} {I J J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
J₁ ∈ π → J₂ ∈ π → J ≤ J₁ → J ≤ J₂ → J₁ = J₂
This theorem states that for any type `ι`, given `I`, `J`, `J₁` and `J₂` as boxes in the `BoxIntegral.Box ι` space and a prepartition `π` of box `I`, if both `J₁` and `J₂` are part of the prepartition `π` and box `J` is less than or equal to both `J₁` and `J₂`, then `J₁` and `J₂` must be equal. Basically, it's stating that if two boxes in a prepartition are both larger than or equal to a certain box, then these two boxes must be the same. This theorem is a property of partitions in the context of integral calculus.
More concisely: If `π` is a prepartition of type `ι`, `J₁`, `J₂` are boxes in `BoxIntegral.Box ι` belonging to `π`, and `J ≤ J₁ ≤ J₂`, then `J₁ = J₂`.
|
BoxIntegral.Prepartition.iUnion_subset
theorem BoxIntegral.Prepartition.iUnion_subset :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion ⊆ ↑I
The theorem `BoxIntegral.Prepartition.iUnion_subset` states that, for any type ι and any box I of type `BoxIntegral.Box ι`, if we have a prepartition π of I, then the union of all boxes in this prepartition (which is denoted by `BoxIntegral.Prepartition.iUnion π`) is a subset of the box I. In other words, the part of I covered by the boxes of the prepartition π does not exceed I.
More concisely: For any box I and prepartition π of I in Lean 4, `BoxIntegral.Prepartition.iUnion π` is a subset of I.
|
BoxIntegral.Prepartition.iUnion_restrict
theorem BoxIntegral.Prepartition.iUnion_restrict :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
(π.restrict J).iUnion = ↑J ∩ π.iUnion
The theorem `BoxIntegral.Prepartition.iUnion_restrict` states that for any prepartition `π` of box `I` in the context of any indexing type `ι`, the union of all boxes within the restricted prepartition of `π` to box `J` is equivalent to the intersection of box `J` and the union of all boxes in prepartition `π`. In other words, when a prepartition `π` of a box `I` is restricted to a box `J`, the portion of `I` covered by this restriction is the same as the intersection of `J` with the portion of `I` covered by the original prepartition `π`.
More concisely: For any prepartition π of a box I and indexing type ι, the restricted prepartition of π to box J equals the intersection of J with the union of boxes in π.
|
BoxIntegral.Prepartition.restrict_boxes_of_le
theorem BoxIntegral.Prepartition.restrict_boxes_of_le :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I),
I ≤ J → (π.restrict J).boxes = π.boxes
This theorem states that if we have a prepartition (a particular division of a box into smaller boxes) of a box 'I', and we restrict this prepartition to a larger box 'J' such that 'I' is less than or equal to 'J', then the set of boxes obtained from the restriction is identical to the set of boxes in the original prepartition. Note that we do not claim that the two prepartitions are the same because they are of different types due to the different boxes they are partitions of.
More concisely: If prepartition P is of box I and subbox J contains I, then the restriction of P to J equals the prepartition of I.
|
BoxIntegral.Prepartition.biUnionIndex_of_mem
theorem BoxIntegral.Prepartition.biUnionIndex_of_mem :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
{πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
J ∈ π → ∀ {J' : BoxIntegral.Box ι}, J' ∈ πi J → π.biUnionIndex πi J' = J
The theorem `BoxIntegral.Prepartition.biUnionIndex_of_mem` states that for every type `ι`, every box `I` and `J` of type `ι`, and every prepartition `π` of `I`, and every function `πi` that assigns a prepartition to every box of type `ι`, if `J` is an element of the prepartition `π` and `J'` is an element of the prepartition `πi J`, then the biUnionIndex of `π` and `πi` for `J'` is equal to `J`. This is a uniqueness property of the `biUnionIndex` method in the `BoxIntegral.Prepartition` class in Lean, expressing that, under the given conditions, the `biUnionIndex` function will always return the same box, `J`, which the function `πi` used to create the prepartition where `J'` is found.
More concisely: Given a type `ι`, a box `I` and `J` of type `ι`, a prepartition `π` of `I`, and a function `πi` assigning partitions to boxes of type `ι`, if `J` belongs to `π` and `J'` belongs to `πi J`, then the biUnionIndex of `π` and `πi` for `J'` equals `J`.
|
BoxIntegral.Prepartition.isPartition_iff_iUnion_eq
theorem BoxIntegral.Prepartition.isPartition_iff_iUnion_eq :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition ↔ π.iUnion = ↑I
This theorem establishes the equivalence between a prepartition `π` of a box `I` being a partition and the union of the boxes in `π` being equal to `I`. In other words, for any type `ι`, any box `I` of type `BoxIntegral.Box ι`, and any prepartition `π` of `I`, `π` is a partition if and only if the union of the sets covered by the boxes of `π` is exactly `I`.
More concisely: A prepartition π of a box I in Lean is equal to its corresponding partition if and only if the union of the boxes in π equals I.
|
BoxIntegral.Prepartition.ext
theorem BoxIntegral.Prepartition.ext :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
(∀ (J : BoxIntegral.Box ι), J ∈ π₁ ↔ J ∈ π₂) → π₁ = π₂
This theorem states that for any type `ι`, any box `I` of type `BoxIntegral.Box ι`, and any two prepartitions `π₁` and `π₂` of this box, if it is the case that for any given box `J` of type `BoxIntegral.Box ι`, `J` is an element of `π₁` if and only if `J` is an element of `π₂`, then these two prepartitions `π₁` and `π₂` are equal. In other words, two prepartitions are identical if they contain exactly the same set of boxes.
More concisely: Two partitions of a box in Lean 4 are equal if and only if they contain the same set of boxes.
|
BoxIntegral.Prepartition.iUnion_top
theorem BoxIntegral.Prepartition.iUnion_top : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι}, ⊤.iUnion = ↑I
This theorem states that for any type `ι` and any given box `I` of type `BoxIntegral.Box ι`, the union of all the boxes in the prepartition `⊤` (the top element in the prepartition) is equivalent to the set represented by the box `I` itself. In other words, if you consider the prepartition that includes every possible box, the union of these boxes covers exactly the same space as the original box `I`.
More concisely: For any type `ι` and `BoxIntegral.Box ι` `I`, the union of all boxes in the prepartition with top element `⊤` is equal to `I`.
|
BoxIntegral.Prepartition.IsPartition.biUnion
theorem BoxIntegral.Prepartition.IsPartition.biUnion :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}
{πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
π.IsPartition → (∀ J ∈ π, (πi J).IsPartition) → (π.biUnion πi).IsPartition
The theorem `BoxIntegral.Prepartition.IsPartition.biUnion` states that for any given type `ι`, box `I` of type `BoxIntegral.Box ι`, prepartition `π` of `I`, and function `πi` which, for every box `J`, gives a prepartition of `J`, if `π` is a partition of `I` and for all `J` in `π`, the prepartition `πi J` is a partition of `J`, then the biUnion of `π` and `πi` is a partition of `I`.
In other words, this theorem assures that a biUnion of partitions, where each element of the primary partition is itself a partition of a subbox, is also a partition of the original box `I`.
More concisely: Given a type `ι`, a box `I` of type `BoxIntegral.Box ι`, a prepartition `π` of `I` that is a partition and for each subbox `J` in `π`, the prepartition `πi J` is a partition of `J`, then the biUnion of `π` and `πi` is a partition of `I`.
|
BoxIntegral.Prepartition.IsPartition.iUnion_eq
theorem BoxIntegral.Prepartition.IsPartition.iUnion_eq :
∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I}, π.IsPartition → π.iUnion = ↑I
The theorem `BoxIntegral.Prepartition.IsPartition.iUnion_eq` states that for any type `ι`, any box `I` of type `ι`, and any prepartition `π` of `I`, if `π` is a partition of `I` (that is, if the boxes of `π` cover the whole `I`), then the union of the boxes of `π` (denoted by `BoxIntegral.Prepartition.iUnion π`) is exactly equal to `I` itself.
More concisely: For any type `ι`, box `I` of type `ι`, and prepartition `π` of `I` that covers `I`, the union of the boxes in `π` equals `I`.
|
BoxIntegral.Prepartition.restrict_mono
theorem BoxIntegral.Prepartition.restrict_mono :
∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
π₁ ≤ π₂ → π₁.restrict J ≤ π₂.restrict J
The theorem `BoxIntegral.Prepartition.restrict_mono` states that for any type `ι`, and any three boxes `I`, `J`, and `π₂` of type `BoxIntegral.Box ι`, and any prepartition `π₁` of the box `I`, if `π₁` is a sub-prepartition of `π₂` (i.e., `π₁ ≤ π₂`), then the restriction of `π₁` to the box `J` is a sub-prepartition of the restriction of `π₂` to the box `J`. In other words, if you restrict a smaller prepartition and a larger prepartition to the same box, the restriction of the smaller prepartition is still smaller than or equal to the restriction of the larger prepartition.
More concisely: For any boxes `I`, `J` of type `BoxIntegral.Box ι`, and prepartitions `π₁ ≤ π₂` of `I`, the restriction of `π₁` to `J` is a sub-prepartition of the restriction of `π₂` to `J`.
|
BoxIntegral.Prepartition.eq_of_mem_of_mem
theorem BoxIntegral.Prepartition.eq_of_mem_of_mem :
∀ {ι : Type u_1} {I J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {x : ι → ℝ},
J₁ ∈ π → J₂ ∈ π → x ∈ J₁ → x ∈ J₂ → J₁ = J₂
This theorem asserts that for any type `ι`, boxes `I`, `J₁`, and `J₂`, and a prepartition `π` of `I`, if `J₁` and `J₂` are both elements of `π` and a point `x` is in both `J₁` and `J₂`, then `J₁` and `J₂` must be the same. Essentially, this is stating that in a prepartition of a box, no point can belong to two distinct sub-boxes.
More concisely: In a prepartition of a box, no point belongs to two distinct sub-boxes.
|