sqrt_div' — Mathlib

English

Let x ∈ ℝ and y ∈ ℝ with y ≥ 0. Then √(x/y) = √x/√y.

Русский

Пусть x ∈ ℝ и y ∈ ℝ, y ≥ 0. Тогда √(x/y) = √x/√y.

LaTeX

$$$\\\\forall x \\\\in \\\\mathbb{R}, \\\\forall y \\\\in \\\\mathbb{R}, y \\\\ge 0 \\\\Rightarrow \\\\sqrt{\\\\frac{x}{y}} = \\\\frac{\\\\sqrt{x}}{\\\\sqrt{y}}$$$

Lean4

@[simp]
theorem sqrt_div' (x) {y : ℝ} (hy : 0 ≤ y) : √(x / y) = √x / √y := by
  rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]

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