Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.continuousWithinAt_rearrangement

Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:165 to 175

Mathematical statement

Exact Lean statement

lemma continuousWithinAt_rearrangement :
    ContinuousWithinAt (rearrangement f · μ) (Set.Ici x) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma continuousWithinAt_rearrangement :    ContinuousWithinAt (rearrangement f · μ) (Set.Ici x) x := by  apply tendsto_order.2 ⟨ fun y hy => _, fun y hy => _ ⟩  · intro y hy    have := lt_rearrangement_iff_lt_distribution.mp hy;    rw [eventually_nhdsWithin_iff]    filter_upwards [gt_mem_nhds this] with b hb hb' using by simpa using lt_rearrangement_iff_lt_distribution.mpr hb  · intro y hy    apply Filter.eventually_of_mem self_mem_nhdsWithin    intro b hb    exact lt_of_le_of_lt (rearrangement_antitone' hb) hy