Measurability of arctan #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[measurability]
theorem
measurable.arctan
{α : Type u_1}
{m : measurable_space α}
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.arctan (f x))