arcsin_projIcc — Mathlib

English

The value of arcsin is unchanged if its input is replaced by its projection onto the interval [−1,1].

Русский

Значение arcsin не меняется при замене аргумента на его проекцию на отрезок [−1,1].

LaTeX

$$$\\arcsin\\left(\\operatorname{projIcc}(-1,1)(x)\\right) = \\arcsin x$$$

Lean4

theorem arcsin_projIcc (x : ℝ) : arcsin (projIcc (-1) 1 (neg_le_self zero_le_one) x) = arcsin x := by
  rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend, Function.comp_apply]

Похожие утверждения