fun_prop

fun_prop は，連続性や可測性など，関数に関する性質を示すタクティクです．

import Mathlib.Tactic

variable {u v : ℝ → ℝ} (hu : Continuous u) (hv : Continuous v)

/-- 連続関数の積は連続関数 -/
example : Continuous (fun x ↦ u x * v x) := by
  fun_prop

/-- 有理関数が可測関数であることを示す -/
example : Measurable fun x : ℝ => (x * x - 1) / x + (x - x * x) := by
  fun_prop