English
There exists a monotone bijection on the nonnegative real numbers whose inverse is squaring; equivalently, the square-root map on NNReal is an order isomorphism with the inverse given by squaring.
Русский
Существует возрастающее биективное отображение на множества неотрицательных действительных чисел, чьим обратным является возведение в квадрат; эквивалентно, отображение квадратного корня на NNReal является порядковым изоморфизмом, у которого обратное — возведение в квадрат.
LaTeX
$$$\text{There exists an order isomorphism } \sqrt: \mathbb{R}_{\ge 0} \to \mathbb{R}_{\ge 0} \text{ with } (\sqrt{x})^2 = x \text{ for all } x \ge 0,\text{ and } \sqrt \text{ is the inverse of } x \mapsto x^2. $$$
Lean4
/-- Square root of a nonnegative real number. -/
@[pp_nodot]
noncomputable def sqrt : ℝ≥0 ≃o ℝ≥0 :=
OrderIso.symm <| powOrderIso 2 two_ne_zero
