Documentation

Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan

Measurability of arctan #

theorem Measurable.arctan {α : Type u_1} {m : MeasurableSpace α} {f : α} (hf : Measurable f) :
Measurable fun (x : α) => Real.arctan (f x)