Documentation

Monlib.Preq.RCLikeLe

Extra lemmas on RCLike #

This file contains extra lemmas on RCLike.

source
theorem RCLike.le_def {K : semiOutParam (Type u_1)} [self : RCLike K] {z : K} {w : K} :
z ≤ w ↔ RCLike.re z ≤ RCLike.re w ∧ RCLike.im z = RCLike.im w

Alias of RCLike.le_iff_re_im.

source
theorem RCLike.lt_def {K : Type u_1} [RCLike K] {z : K} {w : K} :
z < w ↔ RCLike.re z < RCLike.re w ∧ RCLike.im z = RCLike.im w

Alias of RCLike.lt_iff_re_im.

source
theorem RCLike.nonneg_def {K : Type u_1} [RCLike K] {z : K} :
0 ≤ z ↔ 0 ≤ RCLike.re z ∧ RCLike.im z = 0

Alias of RCLike.nonneg_iff.

source
theorem RCLike.pos_def {K : Type u_1} [RCLike K] {z : K} :
0 < z ↔ 0 < RCLike.re z ∧ RCLike.im z = 0

Alias of RCLike.pos_iff.

source
theorem RCLike.nonpos_def {K : Type u_1} [RCLike K] {z : K} :
z ≤ 0 ↔ RCLike.re z ≤ 0 ∧ RCLike.im z = 0

Alias of RCLike.nonpos_iff.

source
theorem RCLike.neg_def {K : Type u_1} [RCLike K] {z : K} :
z < 0 ↔ RCLike.re z < 0 ∧ RCLike.im z = 0

Alias of RCLike.neg_iff.

source
theorem RCLike.nonneg_def' {𝕜 : Type u_1} [RCLike 𝕜] {x : 𝕜} :
0 ≤ x ↔ ↑(RCLike.re x) = x ∧ 0 ≤ RCLike.re x
source
@[simp]
theorem RCLike.real_le_real {𝕜 : Type u_1} [RCLike 𝕜] {x : ℝ} {y : ℝ} :
↑x ≤ ↑y ↔ x ≤ y
source
@[simp]
theorem RCLike.real_lt_real {𝕜 : Type u_1} [RCLike 𝕜] {x : ℝ} {y : ℝ} :
↑x < ↑y ↔ x < y
source
@[simp]
theorem RCLike.zero_le_real {𝕜 : Type u_1} [RCLike 𝕜] {x : ℝ} :
0 ≤ ↑x ↔ 0 ≤ x
source
@[simp]
theorem RCLike.zero_lt_real {𝕜 : Type u_1} [RCLike 𝕜] {x : ℝ} :
0 < ↑x ↔ 0 < x
source
theorem RCLike.not_le_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} {w : 𝕜} :
¬z ≤ w ↔ RCLike.re w < RCLike.re z ∨ RCLike.im z ≠ RCLike.im w
source
theorem RCLike.not_lt_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} {w : 𝕜} :
¬z < w ↔ RCLike.re w ≤ RCLike.re z ∨ RCLike.im z ≠ RCLike.im w
source
theorem RCLike.not_le_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} :
¬z ≤ 0 ↔ 0 < RCLike.re z ∨ RCLike.im z ≠ 0
source
theorem RCLike.not_lt_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {z : 𝕜} :
¬z < 0 ↔ 0 ≤ RCLike.re z ∨ RCLike.im z ≠ 0
source
theorem RCLike.eq_re_ofReal_le {𝕜 : Type u_1} [RCLike 𝕜] {r : ℝ} {z : 𝕜} (hz : ↑r ≤ z) :
z = ↑(RCLike.re z)