sqrt_eq_cases — Mathlib

English

For all real x, y, we have √x = y if and only if (y^2 = x and y ≥ 0) or (x < 0 and y = 0).

Русский

Пусть x, y ∈ ℝ. Тогда √x = y эквивалентно либо y^2 = x и y ≥ 0, либо x < 0 и y = 0.

LaTeX

$$$\sqrt{x} = y \quad\iff\quad (y^2 = x \wedge 0 \le y) \;\lor\; (x < 0 \wedge y = 0)$$$

Lean4

theorem sqrt_eq_cases : √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 :=
  by
  constructor
  · rintro rfl
    rcases le_or_gt 0 x with hle | hlt
    · exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
    · exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
  · rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
    exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

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