Theorems · Theorem · real analysis

BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq

Deprecated since 2026-07-09Use BoxIntegral.Prepartition.injOn_setOfPred_mem_Icc_setOfPred_lower_eq instead.

∀ {ι : 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}

Alias of BoxIntegral.Prepartition.injOn_setOfPred_mem_Icc_setOfPred_lower_eq. An auxiliary lemma used to prove that the same point can't belong to more than 2 ^ Fintype.card ι closed boxes of a prepartition.

Defined in

Mathlib.Analysis.BoxIntegral.Partition.Basic

Cited by

0 results in Mathlib

Foundations

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