mathlib3 documentation

measure_theory.function.special_functions.arctan

Measurability of arctan #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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