equal
deleted
inserted
replaced
402 lemma real_sqrt_le_iff [simp]: "(sqrt x \<le> sqrt y) = (x \<le> y)" |
402 lemma real_sqrt_le_iff [simp]: "(sqrt x \<le> sqrt y) = (x \<le> y)" |
403 unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) |
403 unfolding sqrt_def by (rule real_root_le_iff [OF pos2]) |
404 |
404 |
405 lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)" |
405 lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)" |
406 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) |
406 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2]) |
|
407 |
|
408 lemma real_less_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x < y\<^sup>2 \<Longrightarrow> sqrt x < y" |
|
409 using real_sqrt_less_iff[of x "y\<^sup>2"] by simp |
407 |
410 |
408 lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y" |
411 lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y" |
409 using real_sqrt_le_iff[of x "y\<^sup>2"] by simp |
412 using real_sqrt_le_iff[of x "y\<^sup>2"] by simp |
410 |
413 |
411 lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y" |
414 lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y" |