instContinuousSqrtNNReal — Mathlib

English

There exists a continuous square root operation on NNReal (nonnegative reals).

Русский

Для NNReal существует непрерывная функция sqrt.

LaTeX

$$$\\text{ContinuousSqrt } \\mathbb{R}_{\\ge 0}$$$

Lean4

noncomputable instance : ContinuousSqrt ℝ≥0
    where
  sqrt := NNReal.sqrt ∘ (fun x ↦ x.2 - x.1)
  continuousOn_sqrt := by fun_prop
  sqrt_nonneg := by simp
  sqrt_mul_sqrt := by simpa using fun _ _ h ↦ Eq.symm <| add_tsub_cancel_of_le h

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