Theorems · Definition · real analysis

AbsolutelyContinuousOnInterval.disjWithin

ℝ → ℝ → Set (ℕ × (ℕ → ℝ × ℝ))

The subcollection of all the finite sequences of uIoc intervals consisting of uIoc (a i) (b i), i < n where a i, b i are all in uIcc a b for i < n and uIoc (a i) (b i) are mutually disjoint for i < n. Technically the finite sequence uIoc (a i) (b i), i < n is represented by any E : ℕ × (ℕ → ℝ × ℝ) which satisfies E.1 = n and E.2 i = (a i, b i) for i < n.

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

15 results in Mathlib

Foundations

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