Theorems · Theorem · real analysis

BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany

∀ {ι : Type u_1} {I J Js : BoxIntegral.Box ι} {s : Finset (ι × ℝ)},
  (∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) →
    Js ∈ BoxIntegral.Prepartition.splitMany I s → ¬Disjoint ↑J ↑Js → Js ≤ J

Let s : Finset (ι × ℝ) be a set of hyperplanes {x : ι → ℝ | x i = r} in ι → ℝ encoded as pairs (i, r). Suppose that this set contains all faces of a box J. The hyperplanes of s split a box I into subboxes. Let Js be one of them. If J and Js have nonempty intersection, then Js is a subbox of J.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Split

Cited by

1 results in Mathlib

Foundations

Depth 140 from the axioms · uses propext, Classical.choice, Quot.sound