mathlib documentation

measure_theory.function.special_functions.arctan

Measurability of arctan #

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