Theorems that should exist in Mathlib

Maybe we can create some PRs to mathlib in the future.

More theorems about trigonometric functions in Mathlib

These theorems about trigonometric functions mostly exist in Mathlib in the version of Real.sin, Real.cos or Real.tan but not in the version of Real.Angle.sin, Real.Angle.cos or Real.Angle.tan.

In this section, we will translate these theorems into the version of EuclidGeom.AngValue.sin, EuclidGeom.AngValue.cos or EuclidGeom.AngValue.tan.

@[simp]

theorem EuclidGeom.AngValue.sin_pi_sub {θ : EuclidGeom.AngValue} : EuclidGeom.AngValue.sin (↑Real.pi - θ) = EuclidGeom.AngValue.sin θ

@[simp]

theorem EuclidGeom.AngValue.cos_pi_sub {θ : EuclidGeom.AngValue} : EuclidGeom.AngValue.cos (↑Real.pi - θ) = -EuclidGeom.AngValue.cos θ

theorem EuclidGeom.AngValue.sin_pos_of_zero_lt_toReal_lt_pi {θ : EuclidGeom.AngValue} (h : 0 < EuclidGeom.AngValue.toReal θ) (hp : EuclidGeom.AngValue.toReal θ < Real.pi) : 0 < EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.sin_nonneg_of_toReal_nonneg {θ : EuclidGeom.AngValue} (h : 0 ≤ EuclidGeom.AngValue.toReal θ) : 0 ≤ EuclidGeom.AngValue.sin θ

theorem EuclidGeom.AngValue.sin_neg_of_toReal_neg {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.toReal θ < 0) : EuclidGeom.AngValue.sin θ < 0

theorem EuclidGeom.AngValue.sin_nonpos_of_toReal_nonpos {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.toReal θ ≤ 0) : EuclidGeom.AngValue.sin θ ≤ 0

theorem EuclidGeom.AngValue.cos_pos_of_neg_pi_div_two_lt_of_lt_pi_div_two {θ : EuclidGeom.AngValue} (hn : -Real.pi / 2 < EuclidGeom.AngValue.toReal θ) (h : EuclidGeom.AngValue.toReal θ < Real.pi / 2) : 0 < EuclidGeom.AngValue.cos θ

theorem EuclidGeom.AngValue.cos_nonneg_of_neg_pi_div_two_le_of_le_pi_div_two {θ : EuclidGeom.AngValue} (hn : -Real.pi / 2 ≤ EuclidGeom.AngValue.toReal θ) (h : EuclidGeom.AngValue.toReal θ ≤ Real.pi / 2) : 0 ≤ EuclidGeom.AngValue.cos θ

theorem EuclidGeom.AngValue.cos_neg_of_pi_div_two_lt_toReal {θ : EuclidGeom.AngValue} (h : Real.pi / 2 < EuclidGeom.AngValue.toReal θ) : EuclidGeom.AngValue.cos θ < 0

theorem EuclidGeom.AngValue.cos_neg_of_toReal_lt_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.toReal θ < -Real.pi / 2) : EuclidGeom.AngValue.cos θ < 0

theorem EuclidGeom.AngValue.cos_nonpos_of_pi_div_two_le_toReal {θ : EuclidGeom.AngValue} (h : Real.pi / 2 ≤ EuclidGeom.AngValue.toReal θ) : EuclidGeom.AngValue.cos θ ≤ 0

theorem EuclidGeom.AngValue.cos_nonpos_of_toReal_le_neg_pi_div_two {θ : EuclidGeom.AngValue} (h : EuclidGeom.AngValue.toReal θ ≤ -Real.pi / 2) : EuclidGeom.AngValue.cos θ ≤ 0

theorem EuclidGeom.AngValue.cos_pos_iff {θ : EuclidGeom.AngValue} : 0 < EuclidGeom.AngValue.cos θ ↔ -Real.pi / 2 < EuclidGeom.AngValue.toReal θ ∧ EuclidGeom.AngValue.toReal θ < Real.pi / 2

theorem EuclidGeom.AngValue.cos_neg_iff {θ : EuclidGeom.AngValue} : EuclidGeom.AngValue.cos θ < 0 ↔ EuclidGeom.AngValue.toReal θ < -Real.pi / 2 ∨ Real.pi / 2 < EuclidGeom.AngValue.toReal θ

Compatibility among group, addtorsor and order

class CircularOrderedAddCommGroup (G : Type u_1) extends AddCommGroup , CircularOrder : Type u_1

A circular ordered additive commutative group is an additive commutative group with a circular order whose order is stable under addition and compatiable with negation.

• add : G → G → G
• add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)
• zero : G
• zero_add : ∀ (a : G), 0 + a = a
• add_zero : ∀ (a : G), a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero : ∀ (x : G), AddMonoid.nsmul 0 x = 0
• nsmul_succ : ∀ (n : ℕ) (x : G), AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x
• neg : G → G
• sub : G → G → G
• sub_eq_add_neg : ∀ (a b : G), a - b = a + -b
• zsmul : ℤ → G → G
• zsmul_zero' : ∀ (a : G), SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.ofNat (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : G), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (a : G), -a + a = 0
• add_comm : ∀ (a b : G), a + b = b + a
• btw : G → G → G → Prop
• sbtw : G → G → G → Prop
• btw_refl : ∀ (a : G), btw a a a
• btw_cyclic_left : ∀ {a b c : G}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : G}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : G}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : G}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : G), btw a b c ∨ btw c b a
• btw_add_left : ∀ {a b c : G}, btw a b c → ∀ (g : G), btw (g + a) (g + b) (g + c)
• btw_neg : ∀ {a b c : G}, btw a b c → btw (-a) (-c) (-b)

class CircularOrderedCommGroup (G : Type u_1) extends CommGroup , CircularOrder : Type u_1

A circular ordered commutative group is a commutative group with a circular order whose order is stable under multiplication and compatiable with inverse.

• mul : G → G → G
• mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)
• one : G
• one_mul : ∀ (a : G), 1 * a = a
• mul_one : ∀ (a : G), a * 1 = a
• npow : ℕ → G → G
• npow_zero : ∀ (x : G), Monoid.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : G), Monoid.npow (n + 1) x = x * Monoid.npow n x
• inv : G → G
• div : G → G → G
• div_eq_mul_inv : ∀ (a b : G), a / b = a * b⁻¹
• zpow : ℤ → G → G
• zpow_zero' : ∀ (a : G), DivInvMonoid.zpow 0 a = 1
• zpow_succ' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
• mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
• mul_comm : ∀ (a b : G), a * b = b * a
• btw : G → G → G → Prop
• sbtw : G → G → G → Prop
• btw_refl : ∀ (a : G), btw a a a
• btw_cyclic_left : ∀ {a b c : G}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : G}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : G}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : G}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : G), btw a b c ∨ btw c b a
• btw_mul_left : ∀ {a b c : G}, btw a b c → ∀ (g : G), btw (g * a) (g * b) (g * c)
• btw_inv : ∀ {a b c : G}, btw a b c → btw a⁻¹ c⁻¹ b⁻¹

theorem btw_add_left {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (g + a) (g + b) (g + c)

theorem btw_mul_left {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (g * a) (g * b) (g * c)

@[simp]

theorem btw_add_left_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g + a) (g + b) (g + c) ↔ btw a b c

@[simp]

theorem btw_mul_left_iff {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g * a) (g * b) (g * c) ↔ btw a b c

@[simp]

theorem sbtw_add_left_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g + a) (g + b) (g + c) ↔ sbtw a b c

@[simp]

theorem sbtw_mul_left_iff {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g * a) (g * b) (g * c) ↔ sbtw a b c

theorem sbtw_add_left {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (g + a) (g + b) (g + c)

theorem sbtw_mul_left {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (g * a) (g * b) (g * c)

@[simp]

theorem btw_add_right_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} {g : G} : btw (a + g) (b + g) (c + g) ↔ btw a b c

@[simp]

theorem btw_mul_right_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} {g : G} : btw (a * g) (b * g) (c * g) ↔ btw a b c

theorem btw_add_right {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (a + g) (b + g) (c + g)

theorem btw_mul_right {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (a * g) (b * g) (c * g)

@[simp]

theorem sbtw_add_right_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (a + g) (b + g) (c + g) ↔ sbtw a b c

@[simp]

theorem sbtw_mul_right_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (a * g) (b * g) (c * g) ↔ sbtw a b c

theorem sbtw_add_right {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (a + g) (b + g) (c + g)

theorem sbtw_mul_right {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (a * g) (b * g) (c * g)

theorem btw_neg {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) : btw (-a) (-c) (-b)

theorem btw_inv {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) : btw a⁻¹ c⁻¹ b⁻¹

@[simp]

theorem btw_neg_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : btw (-a) (-b) (-c) ↔ btw a c b

@[simp]

theorem btw_inv_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : btw a⁻¹ b⁻¹ c⁻¹ ↔ btw a c b

theorem btw_neg_iff' {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : btw (-a) (-b) (-c) ↔ btw c b a

theorem btw_inv_iff' {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : btw a⁻¹ b⁻¹ c⁻¹ ↔ btw c b a

theorem btw_neg_iff'' {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : btw (-a) (-b) (-c) ↔ btw b a c

theorem btw_inv_iff'' {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : btw a⁻¹ b⁻¹ c⁻¹ ↔ btw b a c

theorem btw_neg_iff_not_sbtw {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : btw (-a) (-b) (-c) ↔ ¬sbtw a b c

theorem btw_inv_iff_not_sbtw {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : btw a⁻¹ b⁻¹ c⁻¹ ↔ ¬sbtw a b c

theorem not_btw_neg_iff_sbtw {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : ¬btw (-a) (-b) (-c) ↔ sbtw a b c

theorem not_btw_inv_iff_sbtw {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : ¬btw a⁻¹ b⁻¹ c⁻¹ ↔ sbtw a b c

theorem sbtw_neg_iff_not_btw {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : sbtw (-a) (-b) (-c) ↔ ¬btw a b c

theorem sbtw_inv_iff_not_btw {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : sbtw a⁻¹ b⁻¹ c⁻¹ ↔ ¬btw a b c

theorem not_sbtw_neg_iff_btw {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : ¬sbtw (-a) (-b) (-c) ↔ btw a b c

theorem not_sbtw_inv_iff_btw {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : ¬sbtw a⁻¹ b⁻¹ c⁻¹ ↔ btw a b c

@[simp]

theorem sbtw_neg_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : sbtw (-a) (-b) (-c) ↔ sbtw a c b

@[simp]

theorem sbtw_inv_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : sbtw a⁻¹ b⁻¹ c⁻¹ ↔ sbtw a c b

theorem sbtw_neg {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) : sbtw (-a) (-c) (-b)

theorem sbtw_inv {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) : sbtw a⁻¹ c⁻¹ b⁻¹

theorem sbtw_neg_iff' {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : sbtw (-a) (-b) (-c) ↔ sbtw c b a

theorem sbtw_inv_iff' {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : sbtw a⁻¹ b⁻¹ c⁻¹ ↔ sbtw c b a

theorem sbtw_neg_iff'' {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} : sbtw (-a) (-b) (-c) ↔ sbtw b a c

theorem sbtw_inv_iff'' {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} : sbtw a⁻¹ b⁻¹ c⁻¹ ↔ sbtw b a c

theorem btw_sub_left {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (g - a) (g - c) (g - b)

theorem btw_div_left {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (g / a) (g / c) (g / b)

@[simp]

theorem btw_sub_left_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g - a) (g - b) (g - c) ↔ btw a c b

@[simp]

theorem btw_div_left_iff {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g / a) (g / b) (g / c) ↔ btw a c b

theorem btw_sub_left_iff' {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g - a) (g - b) (g - c) ↔ btw c b a

theorem btw_div_left_iff' {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g / a) (g / b) (g / c) ↔ btw c b a

theorem btw_sub_left_iff'' {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g - a) (g - b) (g - c) ↔ btw b a c

theorem btw_div_left_iff'' {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g / a) (g / b) (g / c) ↔ btw b a c

theorem sbtw_sub_left {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (g - a) (g - c) (g - b)

theorem sbtw_div_left {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (g / a) (g / c) (g / b)

@[simp]

theorem sbtw_sub_left_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (g - a) (g - b) (g - c) ↔ sbtw a c b

@[simp]

theorem sbtw_div_left_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (g / a) (g / b) (g / c) ↔ sbtw a c b

theorem sbtw_sub_left_iff' {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g - a) (g - b) (g - c) ↔ sbtw c b a

theorem sbtw_div_left_iff' {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g / a) (g / b) (g / c) ↔ sbtw c b a

theorem sbtw_sub_left_iff'' {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g - a) (g - b) (g - c) ↔ sbtw b a c

theorem sbtw_div_left_iff'' {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g / a) (g / b) (g / c) ↔ sbtw b a c

theorem btw_sub_left_iff_not_sbtw {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g - a) (g - b) (g - c) ↔ ¬sbtw a b c

theorem btw_div_left_iff_not_sbtw {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : btw (g / a) (g / b) (g / c) ↔ ¬sbtw a b c

theorem not_btw_sub_left_iff_sbtw {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : ¬btw (g - a) (g - b) (g - c) ↔ sbtw a b c

theorem not_btw_div_left_iff_sbtw {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : ¬btw (g / a) (g / b) (g / c) ↔ sbtw a b c

theorem sbtw_sub_left_iff_not_btw {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g - a) (g - b) (g - c) ↔ ¬btw a b c

theorem sbtw_div_left_iff_not_btw {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : sbtw (g / a) (g / b) (g / c) ↔ ¬btw a b c

theorem not_sbtw_sub_left_iff_btw {G : Type u_1} [CircularOrderedAddCommGroup G] {g : G} {a : G} {b : G} {c : G} : ¬sbtw (g - a) (g - b) (g - c) ↔ btw a b c

theorem not_sbtw_div_left_iff_btw {G : Type u_1} [CircularOrderedCommGroup G] {g : G} {a : G} {b : G} {c : G} : ¬sbtw (g / a) (g / b) (g / c) ↔ btw a b c

theorem btw_sub_right {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (a - g) (b - g) (c - g)

theorem btw_div_right {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : btw a b c) (g : G) : btw (a / g) (b / g) (c / g)

@[simp]

theorem btw_sub_right_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} {g : G} : btw (a - g) (b - g) (c - g) ↔ btw a b c

@[simp]

theorem btw_div_right_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} {g : G} : btw (a / g) (b / g) (c / g) ↔ btw a b c

theorem sbtw_sub_right {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (a - g) (b - g) (c - g)

theorem sbtw_div_right {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} (h : sbtw a b c) (g : G) : sbtw (a / g) (b / g) (c / g)

@[simp]

theorem sbtw_sub_right_iff {G : Type u_1} [CircularOrderedAddCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (a - g) (b - g) (c - g) ↔ sbtw a b c

@[simp]

theorem sbtw_div_right_iff {G : Type u_1} [CircularOrderedCommGroup G] {a : G} {b : G} {c : G} {g : G} : sbtw (a / g) (b / g) (c / g) ↔ sbtw a b c

instance QuotientAddGroup.instCircularOrderedAddCommGroup (G : Type u_2) [LinearOrderedAddCommGroup G] [Archimedean G] {p : G} [Fact (0 < p)] : CircularOrderedAddCommGroup (G ⧸ AddSubgroup.zmultiples p)

Equations

• One or more equations did not get rendered due to their size.

theorem QuotientAddGroup.sbtw_coe_iff' {G : Type u_2} [LinearOrderedAddCommGroup G] [Archimedean G] {p : G} [hp : Fact (0 < p)] {a : G} {b : G} {c : G} : sbtw ↑a ↑b ↑c ↔ toIocMod (_ : 0 < p) 0 (a - c) < toIcoMod (_ : 0 < p) 0 (b - c)

theorem QuotientAddGroup.sbtw_coe_iff {G : Type u_2} [LinearOrderedAddCommGroup G] [Archimedean G] {p : G} [hp : Fact (0 < p)] {a : G} {b : G} {c : G} : sbtw ↑a ↑b ↑c ↔ toIocMod (_ : 0 < p) c a < toIcoMod (_ : 0 < p) c b

class OrderedAddAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (AddGroup G)] extends AddAction , PartialOrder : Type (max u_1 u_2)

A partial ordered additive group action is a additive group action on a partial order which is stable under the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• vadd_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g +ᵥ a ≤ g +ᵥ b

class OrderedMulAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (Group G)] extends MulAction , PartialOrder : Type (max u_1 u_2)

A partial ordered multiplicative group action is a multiplicative group action on a partial order which is stable under the multiplicative group action.

• smul : G → P → P
• one_smul : ∀ (b : P), 1 • b = b
• mul_smul : ∀ (x y : G) (b : P), (x * y) • b = x • y • b
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• smul_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g • a ≤ g • b

theorem vadd_left_le {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [OrderedAddAction G P] {a : P} {b : P} (h : a ≤ b) (g : G) : g +ᵥ a ≤ g +ᵥ b

theorem smul_left_le {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [OrderedMulAction G P] {a : P} {b : P} (h : a ≤ b) (g : G) : g • a ≤ g • b

@[simp]

theorem vadd_left_le_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [OrderedAddAction G P] {g : G} {a : P} {b : P} : g +ᵥ a ≤ g +ᵥ b ↔ a ≤ b

@[simp]

theorem smul_left_le_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [OrderedMulAction G P] {g : G} {a : P} {b : P} : g • a ≤ g • b ↔ a ≤ b

@[simp]

theorem vadd_left_lt_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [OrderedAddAction G P] {g : G} {a : P} {b : P} : g +ᵥ a < g +ᵥ b ↔ a < b

@[simp]

theorem smul_left_lt_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [OrderedMulAction G P] {g : G} {a : P} {b : P} : g • a < g • b ↔ a < b

theorem vadd_left_lt {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [OrderedAddAction G P] {a : P} {b : P} (h : a < b) (g : G) : g +ᵥ a < g +ᵥ b

theorem smul_left_lt {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [OrderedMulAction G P] {a : P} {b : P} (h : a < b) (g : G) : g • a < g • b

class LinearOrderedAddAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (AddGroup G)] extends OrderedAddAction , Min , Max , Ord : Type (max u_1 u_2)

A linearly ordered additive group action is an additive group action on a linearly order which is stable under the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• vadd_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g +ᵥ a ≤ g +ᵥ b
• min : P → P → P
• max : P → P → P
• compare : P → P → Ordering
• le_total : ∀ (a b : P), a ≤ b ∨ b ≤ a

  A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : P) => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq P

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : P) => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : P), min a b = if a ≤ b then a else b

  The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : P), max a b = if a ≤ b then b else a

  The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : P), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

class LinearOrderedMulAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (Group G)] extends OrderedMulAction , Min , Max , Ord : Type (max u_1 u_2)

A linearly ordered multiplicative group action is a multiplicative group action on a linearly order which is stable under the multiplicative group action.

• smul : G → P → P
• one_smul : ∀ (b : P), 1 • b = b
• mul_smul : ∀ (x y : G) (b : P), (x * y) • b = x • y • b
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• smul_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g • a ≤ g • b
• min : P → P → P
• max : P → P → P
• compare : P → P → Ordering
• le_total : ∀ (a b : P), a ≤ b ∨ b ≤ a

  A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : P) => x ≤ x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq : DecidableEq P

  In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : P) => x < x_1

  In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : P), min a b = if a ≤ b then a else b

  The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : P), max a b = if a ≤ b then b else a

  The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : P), compare a b = compareOfLessAndEq a b

  Comparison via compare is equal to the canonical comparison given decidable < and =.

theorem min_vadd {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [LinearOrderedAddAction G P] {a : P} {b : P} (g : G) : min (g +ᵥ a) (g +ᵥ b) = g +ᵥ min a b

theorem min_smul {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [LinearOrderedMulAction G P] {a : P} {b : P} (g : G) : min (g • a) (g • b) = g • min a b

theorem max_vadd {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [LinearOrderedAddAction G P] {a : P} {b : P} (g : G) : max (g +ᵥ a) (g +ᵥ b) = g +ᵥ max a b

theorem max_smul {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [LinearOrderedMulAction G P] {a : P} {b : P} (g : G) : max (g • a) (g • b) = g • max a b

class CircularOrderedAddAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (AddGroup G)] extends AddAction , CircularOrder : Type (max u_1 u_2)

A circular ordered additive group action is an additive group action on a circular order which is stable under the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• btw : P → P → P → Prop
• sbtw : P → P → P → Prop
• btw_refl : ∀ (a : P), btw a a a
• btw_cyclic_left : ∀ {a b c : P}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : P}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : P}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : P}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : P), btw a b c ∨ btw c b a
• btw_vadd_left : ∀ {a b c : P}, btw a b c → ∀ (g : G), btw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c)

class CircularOrderedMulAction (G : outParam (Type u_1)) (P : Type u_2) [outParam (Group G)] extends MulAction , CircularOrder : Type (max u_1 u_2)

A circular ordered multiplicative group action is a multiplicative group action on a circular order which is stable under the multiplicative group action.

• smul : G → P → P
• one_smul : ∀ (b : P), 1 • b = b
• mul_smul : ∀ (x y : G) (b : P), (x * y) • b = x • y • b
• btw : P → P → P → Prop
• sbtw : P → P → P → Prop
• btw_refl : ∀ (a : P), btw a a a
• btw_cyclic_left : ∀ {a b c : P}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : P}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : P}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : P}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : P), btw a b c ∨ btw c b a
• btw_smul_left : ∀ {a b c : P}, btw a b c → ∀ (g : G), btw (g • a) (g • b) (g • c)

theorem btw_vadd_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [CircularOrderedAddAction G P] {a : P} {b : P} {c : P} (h : btw a b c) (g : G) : btw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c)

theorem btw_smul_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [CircularOrderedMulAction G P] {a : P} {b : P} {c : P} (h : btw a b c) (g : G) : btw (g • a) (g • b) (g • c)

@[simp]

theorem btw_vadd_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [CircularOrderedAddAction G P] {g : G} {a : P} {b : P} {c : P} : btw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c) ↔ btw a b c

@[simp]

theorem btw_smul_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [CircularOrderedMulAction G P] {g : G} {a : P} {b : P} {c : P} : btw (g • a) (g • b) (g • c) ↔ btw a b c

@[simp]

theorem sbtw_vadd_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [CircularOrderedAddAction G P] {g : G} {a : P} {b : P} {c : P} : sbtw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c) ↔ sbtw a b c

@[simp]

theorem sbtw_smul_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [CircularOrderedMulAction G P] {g : G} {a : P} {b : P} {c : P} : sbtw (g • a) (g • b) (g • c) ↔ sbtw a b c

theorem sbtw_vadd_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (AddGroup G)] [CircularOrderedAddAction G P] {a : P} {b : P} {c : P} (h : sbtw a b c) (g : G) : sbtw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c)

theorem sbtw_smul_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (Group G)] [CircularOrderedMulAction G P] {a : P} {b : P} {c : P} (h : sbtw a b c) (g : G) : sbtw (g • a) (g • b) (g • c)

class OrderedAddTorsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (OrderedAddCommGroup G)] extends OrderedAddAction , VSub : Type (max u_1 u_2)

A partial ordered AddTorsor is an AddTorsor with partial orders on the group and the type acted on, such that both orders are compatiable with the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• vadd_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g +ᵥ a ≤ g +ᵥ b
• vsub : P → P → G
• nonempty : Nonempty P
• vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1

  Torsor subtraction and addition with the same element cancels out.

• vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

  Torsor addition and subtraction with the same element cancels out.

• vadd_right_le : ∀ {f g : G}, f ≤ g → ∀ (a : P), f +ᵥ a ≤ g +ᵥ a

theorem vadd_right_le {G : outParam (Type u_1)} {P : Type u_2} [outParam (OrderedAddCommGroup G)] [OrderedAddTorsor G P] {f : G} {g : G} (h : f ≤ g) (a : P) : f +ᵥ a ≤ g +ᵥ a

theorem vadd_right_lt {G : outParam (Type u_1)} {P : Type u_2} [outParam (OrderedAddCommGroup G)] [OrderedAddTorsor G P] {f : G} {g : G} (h : f < g) (a : P) : f +ᵥ a < g +ᵥ a

class LinearOrderedAddTorsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (LinearOrderedAddCommGroup G)] extends LinearOrderedAddAction , VSub : Type (max u_1 u_2)

A linearly ordered AddTorsor is an AddTorsor with linearly orders on the group and the type acted on, such that both orders are compatiable with the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• le : P → P → Prop
• lt : P → P → Prop
• le_refl : ∀ (a : P), a ≤ a
• le_trans : ∀ (a b c : P), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : P), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : P), a ≤ b → b ≤ a → a = b
• vadd_left_le : ∀ {a b : P}, a ≤ b → ∀ (g : G), g +ᵥ a ≤ g +ᵥ b
• min : P → P → P
• max : P → P → P
• compare : P → P → Ordering
• le_total : ∀ (a b : P), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : P) => x ≤ x_1
• decidableEq : DecidableEq P
• decidableLT : DecidableRel fun (x x_1 : P) => x < x_1
• min_def : ∀ (a b : P), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : P), max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : P), compare a b = compareOfLessAndEq a b
• vsub : P → P → G
• nonempty : Nonempty P
• vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1

  Torsor subtraction and addition with the same element cancels out.

• vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

  Torsor addition and subtraction with the same element cancels out.

• vadd_right_le : ∀ {f g : G}, f ≤ g → ∀ (a : P), f +ᵥ a ≤ g +ᵥ a

@[simp]

theorem vadd_right_le_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {f : G} {g : G} {a : P} : f +ᵥ a ≤ g +ᵥ a ↔ f ≤ g

@[simp]

theorem vadd_right_lt_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {f : G} {g : G} {a : P} : f +ᵥ a < g +ᵥ a ↔ f < g

@[simp]

theorem vsub_right_le_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {a : P} {b : P} {x : P} : a -ᵥ x ≤ b -ᵥ x ↔ a ≤ b

theorem vsub_right_le {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {a : P} {b : P} (h : a ≤ b) (x : P) : a -ᵥ x ≤ b -ᵥ x

@[simp]

theorem vsub_left_le_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {x : P} {a : P} {b : P} : x -ᵥ a ≤ x -ᵥ b ↔ b ≤ a

theorem vsub_left_le {G : outParam (Type u_1)} {P : Type u_2} [outParam (LinearOrderedAddCommGroup G)] [LinearOrderedAddTorsor G P] {a : P} {b : P} (h : a ≤ b) (x : P) : x -ᵥ b ≤ x -ᵥ a

class CircularOrderedAddTorsor (G : outParam (Type u_1)) (P : Type u_2) [outParam (CircularOrderedAddCommGroup G)] extends CircularOrderedAddAction , VSub : Type (max u_1 u_2)

A circular ordered AddTorsor is an AddTorsor with circular orders on the group and the type acted on, such that both orders are compatiable with the additive group action.

• vadd : G → P → P
• zero_vadd : ∀ (p : P), 0 +ᵥ p = p
• add_vadd : ∀ (g₁ g₂ : G) (p : P), g₁ + g₂ +ᵥ p = g₁ +ᵥ (g₂ +ᵥ p)
• btw : P → P → P → Prop
• sbtw : P → P → P → Prop
• btw_refl : ∀ (a : P), btw a a a
• btw_cyclic_left : ∀ {a b c : P}, btw a b c → btw b c a
• sbtw_iff_btw_not_btw : ∀ {a b c : P}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a
• sbtw_trans_left : ∀ {a b c d : P}, sbtw a b c → sbtw b d c → sbtw a d c
• btw_antisymm : ∀ {a b c : P}, btw a b c → btw c b a → a = b ∨ b = c ∨ c = a
• btw_total : ∀ (a b c : P), btw a b c ∨ btw c b a
• btw_vadd_left : ∀ {a b c : P}, btw a b c → ∀ (g : G), btw (g +ᵥ a) (g +ᵥ b) (g +ᵥ c)
• vsub : P → P → G
• nonempty : Nonempty P
• vsub_vadd' : ∀ (p1 p2 : P), p1 -ᵥ p2 +ᵥ p2 = p1

  Torsor subtraction and addition with the same element cancels out.

• vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

  Torsor addition and subtraction with the same element cancels out.

• btw_vadd_right : ∀ {e f g : G}, btw e f g → ∀ (a : P), btw (e +ᵥ a) (f +ᵥ a) (g +ᵥ a)

theorem btw_vadd_right {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {e : G} {f : G} {g : G} (h : btw e f g) (a : P) : btw (e +ᵥ a) (f +ᵥ a) (g +ᵥ a)

theorem sbtw_vadd_right {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {e : G} {f : G} {g : G} (h : sbtw e f g) (a : P) : sbtw (e +ᵥ a) (f +ᵥ a) (g +ᵥ a)

@[simp]

theorem btw_vadd_right_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {e : G} {f : G} {g : G} {a : P} : btw (e +ᵥ a) (f +ᵥ a) (g +ᵥ a) ↔ btw e f g

@[simp]

theorem sbtw_vadd_right_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {e : G} {f : G} {g : G} {a : P} : sbtw (e +ᵥ a) (f +ᵥ a) (g +ᵥ a) ↔ sbtw e f g

@[simp]

theorem btw_vsub_right_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} {x : P} : btw (a -ᵥ x) (b -ᵥ x) (c -ᵥ x) ↔ btw a b c

theorem btw_vsub_right {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} (h : btw a b c) (x : P) : btw (a -ᵥ x) (b -ᵥ x) (c -ᵥ x)

@[simp]

theorem sbtw_vsub_right_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} {x : P} : sbtw (a -ᵥ x) (b -ᵥ x) (c -ᵥ x) ↔ sbtw a b c

theorem sbtw_vsub_right {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} (h : sbtw a b c) (x : P) : sbtw (a -ᵥ x) (b -ᵥ x) (c -ᵥ x)

@[simp]

theorem btw_vsub_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : btw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ btw a c b

theorem btw_vsub_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} (h : btw a b c) (x : P) : btw (x -ᵥ a) (x -ᵥ c) (x -ᵥ b)

theorem btw_vsub_left_iff' {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : btw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ btw c b a

theorem btw_vsub_left_iff'' {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : btw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ btw b a c

theorem btw_vsub_left_iff_not_sbtw {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : btw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ ¬sbtw a b c

theorem not_btw_vsub_left_iff_sbtw {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : ¬btw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ sbtw a b c

theorem sbtw_vsub_left_iff_not_btw {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : sbtw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ ¬btw a b c

theorem not_sbtw_vsub_left_iff_btw {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : ¬sbtw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ btw a b c

@[simp]

theorem sbtw_vsub_left_iff {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {x : P} {a : P} {b : P} {c : P} : sbtw (x -ᵥ a) (x -ᵥ b) (x -ᵥ c) ↔ sbtw a c b

theorem sbtw_vsub_left {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [CircularOrderedAddTorsor G P] {a : P} {b : P} {c : P} (h : sbtw a b c) (x : P) : sbtw (x -ᵥ a) (x -ᵥ c) (x -ᵥ b)

theorem vsub_nonpos_iff_vsub_rev_nonneg {G : outParam (Type u_1)} {P : Type u_2} [outParam (OrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) : a -ᵥ b ≤ 0 ↔ 0 ≤ b -ᵥ a

theorem vsub_neg_iff_vsub_rev_pos {G : outParam (Type u_1)} {P : Type u_2} [outParam (OrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) : a -ᵥ b < 0 ↔ 0 < b -ᵥ a

theorem btw_vsub_fst_iff_btw_vsub_snd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : btw 0 (b -ᵥ a) (c -ᵥ a) ↔ btw (a -ᵥ b) 0 (c -ᵥ b)

theorem btw_vsub_fst_iff_btw_vsub_trd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : btw 0 (b -ᵥ a) (c -ᵥ a) ↔ btw (a -ᵥ c) (b -ᵥ c) 0

theorem btw_vsub_snd_iff_btw_vsub_trd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : btw (a -ᵥ b) 0 (c -ᵥ b) ↔ btw (a -ᵥ c) (b -ᵥ c) 0

theorem sbtw_vsub_fst_iff_sbtw_vsub_snd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : sbtw 0 (b -ᵥ a) (c -ᵥ a) ↔ sbtw (a -ᵥ b) 0 (c -ᵥ b)

theorem sbtw_vsub_fst_iff_sbtw_vsub_trd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : sbtw 0 (b -ᵥ a) (c -ᵥ a) ↔ sbtw (a -ᵥ c) (b -ᵥ c) 0

theorem sbtw_vsub_snd_iff_sbtw_vsub_trd {G : outParam (Type u_1)} {P : Type u_2} [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] (a : P) (b : P) (c : P) : sbtw (a -ᵥ b) 0 (c -ᵥ b) ↔ sbtw (a -ᵥ c) (b -ᵥ c) 0

def AddTorsor.OrderedAddTorsor_of_OrderedAddCommGroup (G : outParam (Type u_1)) (P : Type u_2) [outParam (OrderedAddCommGroup G)] [AddTorsor G P] : OrderedAddTorsor G P

If the group acting on an AddTorsor is a partial ordered group, then there is a natual partial order on the AddTorsor along with a corresponding structure of partial ordered AddTorsor induced by the partial ordered group. This is not an instance, since we do not want it to conflict with other partial order structures that may exist on the AddTorsor.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AddTorsor.LinearOrderedAddTorsor_of_LinearOrderedAddCommGroup (G : outParam (Type u_1)) (P : Type u_2) [outParam (LinearOrderedAddCommGroup G)] [AddTorsor G P] : LinearOrderedAddTorsor G P

If the group acting on an AddTorsor is a linearly ordered group, then there is a natual linearly order on the AddTorsor along with a corresponding structure of linearly ordered AddTorsor induced by the linearly ordered group. This is not an instance, since we do not want it to conflict with other linearly order structures that may exist on the AddTorsor.

Equations

• One or more equations did not get rendered due to their size.

def AddTorsor.CircularOrderedAddTorsor_of_CircularOrderedAddCommGroup (G : outParam (Type u_1)) (P : Type u_2) [outParam (CircularOrderedAddCommGroup G)] [AddTorsor G P] : CircularOrderedAddTorsor G P

If the group acting on an AddTorsor is a circular ordered group, then there is a natual circular order on the AddTorsor along with a corresponding structure of circular ordered AddTorsor induced by the circular ordered group. This is not an instance, since we do not want it to conflict with other circular order structures that may exist on the AddTorsor.

Equations

• One or more equations did not get rendered due to their size.

More theorems about real numbers divided by nature numbers

theorem Real.div_nat_le_self_of_nonnneg {a : ℝ} (n : ℕ) (h : 0 ≤ a) : a / ↑n ≤ a

theorem Real.div_nat_le_self_of_pos {a : ℝ} (n : ℕ) (h : 0 < a) : a / ↑n ≤ a

theorem Real.div_nat_lt_self_of_pos_of_two_le {a : ℝ} {n : ℕ} (h : 0 < a) (hn : 2 ≤ n) : a / ↑n < a

theorem Real.div_eq_div_of_div_eq_div {a : ℝ} {b : ℝ} {c : ℝ} {d : ℝ} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / b = c / d) : a / c = b / d

theorem pi_div_nat_nonneg (n : ℕ) : 0 ≤ Real.pi / ↑n