Skip to content

Commit

Permalink
Whitespace
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Nov 19, 2024
1 parent b63f777 commit b7d849b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
Original file line number Diff line number Diff line change
Expand Up @@ -198,7 +198,7 @@ theorem ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ [SigmaFinite μ]
have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by
simp only [ENNReal.coe_natCast]
exact ENNReal.tendsto_nat_nhds_top
this.eventually_const_le (hx.trans_le le_top)
this.eventually_const_le (hx.trans_le le_top)
apply Set.mem_iUnion.2
exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists
refine le_antisymm ?_ bot_le
Expand Down

0 comments on commit b7d849b

Please sign in to comment.