exact self_mem_nhdsWithin
case inr.refine_2.intro.intro.intro.intro.intro.inr.inr.refine_2.refine_3
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
hm_lt : f m < (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM_lt : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z < f M
⊢ s ∈ nhdsWithin m s
no goals