arcsin_inj — Mathlib

English

For x,y ∈ [−1,1], arcsin x = arcsin y if and only if x = y.

Русский

Для x,y ∈ [−1,1] выполняется arcsin x = arcsin y тогда и только тогда, когда x = y.

LaTeX

$$$\\arcsin x = \\arcsin y \\Leftrightarrow x = y \\text{ для } x,y \in [-1,1]$$$

Lean4

theorem arcsin_inj {x y : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) (hy₁ : -1 ≤ y) (hy₂ : y ≤ 1) : arcsin x = arcsin y ↔ x = y :=
  injOn_arcsin.eq_iff ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩

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