Theorem Real.measurable_arctan

Modification history

2023-06-07 00:58

Mathlib/MeasureTheory/Function/SpecialFunctions/Arctan.lean

feat: port MeasureTheory.Function.SpecialFunctions.Arctan (#4754)

Added Real.measurable_arctan View on Github →