Skip to content

Commit c85e85f

Browse files
committed
style(Analysis/SpecialFunctions/FrullaniIntegral): tiny clean up
1 parent 8837782 commit c85e85f

1 file changed

Lines changed: 1 addition & 5 deletions

File tree

Mathlib/Analysis/SpecialFunctions/FrullaniIntegral.lean

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,14 +22,10 @@ integrability of the integrand.
2222

2323
public section
2424

25-
open Real Set Filter MeasureTheory intervalIntegral
26-
27-
open scoped Topology
25+
open Real Set Filter MeasureTheory intervalIntegral Topology Metric
2826

2927
namespace Frullani
3028

31-
open Metric
32-
3329
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E}
3430
{a b c : ℝ} {L R : E}
3531

0 commit comments

Comments
 (0)