mathlib documentation

measure_theory.function.special_functions.arctan

Measurability of arctan #

@[measurability]
@[measurability]
theorem measurable.arctan {α : Type u_1} {m : measurable_space α} {f : α } (hf : measurable f) :
measurable (λ (x : α), real.arctan (f x))