Theorems · Theorem · real analysis

BoxIntegral.Prepartition.injOn_setOfPred_mem_Icc_setOfPred_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}

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

2 results in Mathlib

Foundations

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