Theorems · Theorem · measure theory

Real.ContinuousOn.eq_of_eqOn_Ioo

∀ {f : ℝ → ℝ} {c r R : ℝ}, ContinuousOn f (Set.Ioc r R) → r < R → Set.EqOn f (fun x => c) (Set.Ioo r R) → f R = c

Companion lemma to ContinuousOn.circleAverage: a function continuous on Ioc r R and constant on Ioo r R is constant.

Defined in

Mathlib.MeasureTheory.Integral.CircleAverage

Cited by

2 results in Mathlib

Foundations

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