EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent
theorem EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 ∧ EuclideanGeometry.oangle p₁ p₂ p₃ ≠ ↑Real.pi ↔
AffineIndependent ℝ ![p₁, p₂, p₃]
The theorem `EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent` states that, given a metric space `P` with an associated normed add commutative group `V` that has an inner product space structure over the real numbers, and is two-dimensional, and oriented. For any three distinct points `p₁`, `p₂`, `p₃` in `P`, the oriented angle (according to the Euclidean geometry) formed by these three points is not equal to zero and is not equal to pi if and only if the set of these three points is affinely independent over the real numbers. Affine independence here means that no nontrivial weighted sum of these points, where the sum of weights is zero, yields the zero vector.
More concisely: In a two-dimensional oriented metric space with an inner product, three distinct points form a non-zero and non-π angle according to Euclidean geometry if and only if they are affinely independent.
|
EuclideanGeometry.oangle_sub_left
theorem EuclideanGeometry.oangle_sub_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ p₃ : P},
p₁ ≠ p →
p₂ ≠ p →
p₃ ≠ p →
EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₂ p p₃
The theorem `EuclideanGeometry.oangle_sub_left` states that given a 2-dimensional vector space `V` over the real numbers `ℝ` and a metric space `P` which is a normed additive torsor for `V`, for any four distinct points `p`, `p₁`, `p₂`, and `p₃` in `P`, the difference between the angle at `p` between `p₁` and `p₃` and the angle at `p` between `p₁` and `p₂` equals the angle at `p` between `p₂` and `p₃`. This is a fundamental property of angles in Euclidean geometry, expressing that the change in angle at a point as you move from one line to another is independent of the path taken.
More concisely: For any 2-dimensional real vector space `V` and a normed additive torsor `P` over `V`, the difference between angles at a point `p` in `P` between vectors `p₁-p` and `p₂-p` is equal to the difference between angles at `p` between `p₂-p` and `p₃-p`.
|
EuclideanGeometry.oangle_midpoint_rev_right
theorem EuclideanGeometry.oangle_midpoint_rev_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₂ p₃) = EuclideanGeometry.oangle p₁ p₂ p₃
This theorem states that in a 2-dimensional inner product space with a normed additive commutative group structure, metric space, and a normed additive Torsor, the oriented angle at a point 'p₁' with respect to points 'p₂' and 'p₃' remains the same if 'p₃' is replaced by the midpoint of the segment between 'p₂' and 'p₃'. This is applicable when the space is oriented over the real numbers. In simple terms, it means that the angle measured from 'p₁' to 'p₂' and then to the midpoint of 'p₂' and 'p₃' is the same as the angle measured from 'p₁' to 'p₂' and then to 'p₃'.
More concisely: In a 2-dimensional real inner product space with a normed additive commutative group structure and a normed additive Torsor, the oriented angle from a point to another and then to the midpoint of the segment between them is constant.
|
Sbtw.oangle_eq_add_pi_left
theorem Sbtw.oangle_eq_add_pi_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₁' p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₁' → p₃ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃ + ↑Real.pi
This theorem states that in a normed add commutative group `V` that forms an inner product space over the real numbers `ℝ` and a metric space `P` equipped with a normed add torsor `V P`, with `V` being a 2-dimensional real vector space, if a point `p₂` strictly lies between `p₁` and `p₁'` in the real number line, and `p₃` is not equal to `p₂`, then the oriented angle between points `p₁`, `p₂`, and `p₃` is the sum of the oriented angle between points `p₁'`, `p₂`, and `p₃`, and the constant π. Essentially, it states that replacing the first point of an oriented angle by a point on the same line, but the opposite ray, adds a quantity of π to the original angle.
More concisely: In a 2-dimensional real inner product space `V` and a normed add torsor `V P`, if `p₁`, `p₂`, and `p₃` are points on the real number line with `p₂` strictly between `p₁` and `p₁'`, then the oriented angle between `p₁`, `p₂`, and `p₃` equals the sum of the oriented angle between `p₁'`, `p₂`, and `p₃` and π.
|
EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero
theorem EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = 0
This theorem states that in a two-dimensional oriented Euclidean space, the oriented angle formed by three points `p₁`, `p₂`, and `p₃` is zero if and only if the oriented angle formed by the points in reverse order, `p₃`, `p₂`, and `p₁`, is also zero. Here, an oriented angle is an angle with a defined order of the points, i.e., the angle is considered positive if the points occur in a certain order and negative if they occur in the opposite order. The angle is measured in an inner product space over the real numbers, with `V` being a normed add commutative group, `P` a metric space, and `V` acting on `P` by translations.
More concisely: In a two-dimensional oriented Euclidean space, the oriented angles formed by points `p₁`, `p₂`, and `p₃`, and `p₃`, `p₂`, and `p₁` are equal.
|
EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi
theorem EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi
The theorem `EuclideanGeometry.oangle_eq_pi_iff_oangle_rev_eq_pi` states that for any three points `p₁`, `p₂`, and `p₃` in a Euclidean geometry space `P`, which is endowed with a normed addition group `V` (a vector space) with inner product space over real numbers `ℝ`, the oriented angle formed by `p₁`, `p₂`, and `p₃` is equal to π (defined as twice a zero of cosine function) if and only if the oriented angle formed by reversing the order of the points to `p₃`, `p₂`, `p₁` is also equal to π. This is true in the context that `V` is a 2-dimensional vector space over `ℝ` and is oriented.
More concisely: In a 2-dimensional Euclidean geometry space with inner product over the real numbers, the oriented angle between three points is equal to π if and only if the oriented angle formed by reversing their order is also equal to π.
|
Sbtw.oangle_sign_eq
theorem Sbtw.oangle_sign_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (p₄ : P),
Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₂ p₄ p₃).sign
This theorem states that for a given four points where the first three points are in strict order on the same line in a two-dimensional Euclidean space with an inner product, the sign of the angle at the fourth point between the first and second points is equal to the sign of the angle at the fourth point between the second and third points. This essentially implies that the fourth point sees the three points in the same order along the line.
More concisely: For points P, Q, R, and S on a line in a 2-dimensional Euclidean space with an inner product, if the angle between PQ and QR is of the same sign as the angle between QR and RS, then the points lie on the same line.
|
EuclideanGeometry.oangle_self_left_right
theorem EuclideanGeometry.oangle_self_left_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₂ p₁ = 0
This theorem, named `EuclideanGeometry.oangle_self_left_right`, is about the angle formed at a point in Euclidean geometry. Specifically, it states that for any two points `p₁` and `p₂` in a Euclidean space defined over the real numbers with a two-dimensional vector space as an affine space, the angle `∡p₁p₂p₁` (i.e., the angle formed at `p₁` with `p₂` and `p₁` as the end points of the two rays) is always `0`. This is based on the standard definition of an angle in geometry, where an angle formed by two identical rays (in this case the rays `p₁p₂` and `p₁p₁`) is always `0`.
More concisely: In Euclidean geometry, the angle formed at a point by two identical rays is zero.
|
EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.left_ne_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₁ ≠ p₂
This theorem, stated in the context of Euclidean Geometry, asserts that given a normed additive commutative group `V` equipped with an inner product space structure over the real numbers, a metric space `P`, and a normed additive torsor `V` over `P`, if the space `V` has a two-dimensional real vector space structure and is oriented, then for any three points `p₁`, `p₂`, and `p₃` in `P`, if the angle between these three points is equal to `π / 2`, then the first two points `p₁` and `p₂` must be distinct, that is, they are not the same point.
More concisely: In Euclidean Geometry, if a two-dimensional oriented inner product space over the real numbers with distinct points `p₁` and `p₂` is a normed additive torsor over a metric space, then `p₁` and `p₂` are distinct when the angle between them is a right angle (π/2 radians).
|
EuclideanGeometry.right_ne_of_oangle_eq_pi
theorem EuclideanGeometry.right_ne_of_oangle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi → p₃ ≠ p₂
This theorem is a statement about Euclidean geometry, specifically in the context of inner product spaces. It says that if you have three points in a two-dimensional Euclidean space (which is implied by the fact that the rank of the underlying vector space is 2), oriented in a certain way, and the angle between the first point and the line joining the other two points is equal to π (the mathematical constant representing the ratio of a circle's circumference to its diameter), then the last two points cannot be the same point. In other words, you can't have an angle of π between a point and itself. This is essentially a formal way of saying that straight angles (angles of π radians) can't form at a single point.
More concisely: In a two-dimensional Euclidean space, if the angle between two line segments with a common endpoint is π radians, then the other endpoints of the segments are distinct.
|
EuclideanGeometry.left_ne_of_oangle_ne_zero
theorem EuclideanGeometry.left_ne_of_oangle_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₁ ≠ p₂
This theorem states that in a 2-dimensional oriented module over the real numbers, where the module is a normed add commutative group and also an inner product space, and where points lie in a metric space equipped with a normed add torsor structure, if the angle between three points is nonzero, then the first two points cannot be the same. Here, the angle is measured in the sense of Euclidean geometry. Thus, in simple terms, no two distinct points can make a nonzero angle with a common third point while being identical themselves.
More concisely: In a 2-dimensional oriented real normed add commutative group and inner product space with metric space structure, distinct points make a nonzero angle if and only if they are not identical.
|
Wbtw.oangle_eq_right
theorem Wbtw.oangle_eq_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₃' : P},
Wbtw ℝ p₂ p₃ p₃' → p₃ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'
The theorem `Wbtw.oangle_eq_right` states that in a two-dimensional oriented vector space over the real numbers, if we have four points `p₁`, `p₂`, `p₃`, and `p₃'` such that `p₃` and `p₃'` lie on the same ray from `p₂` with `p₃'` weakly further away, then the oriented angle from `p₁` to `p₂` to `p₃` is the same as the oriented angle from `p₁` to `p₂` to `p₃'`, provided that `p₂` is not equal to `p₃`. The concept of weakly betweenness, denoted by `Wbtw`, means that `p₃` lies in the affine segment between `p₂` and `p₃'`. An important condition here is that the dimension of the vector space is exactly 2. The oriented angle is determined with respect to the orientation of the vector space.
More concisely: In a 2-dimensional oriented real vector space, if points $p\_1, p\_2, p\_3,$ and $p\_3'$ lie on the same ray from $p\_2$ with $p\_3'$ weakly further away than $p\_3$, and $p\_2$ is distinct from $p\_3$, then the oriented angle from $p\_1$ to $p\_2$ to $p\_3$ equals the oriented angle from $p\_1$ to $p\_2$ to $p\_3'$.
|
EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq
theorem EuclideanGeometry.collinear_iff_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆ →
(Collinear ℝ {p₁, p₂, p₃} ↔ Collinear ℝ {p₄, p₅, p₆})
The theorem states that given two sets of three points each, in a two-dimensional Euclidean space with an orientation, if the orientations of the angles formed by each set, when doubled, are equal; then the property of being collinear (i.e., all three points lying on the same line) is equivalent for both sets. This means that if one set of three points is collinear, then the other set must also be collinear, and vice versa.
More concisely: If two sets of three points in a 2D Euclidean space with an orientation have the same signed angle sums, then the sets are collinear.
|
Sbtw.oangle₃₂₁_eq_pi
theorem Sbtw.oangle₃₂₁_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₂ p₁ = ↑Real.pi
This theorem states that if you have three points in a two-dimensional real inner product space, and the second point is strictly between the first and third points, then the oriented angle formed by these points at the second point, when taken in reverse order, is equal to π (Pi). The oriented angle is calculated using the Euclidean geometry concept in a space which is a metric space and a normed add torsor over a normed add comm group. The space is also oriented with 2-dimensional real vectors.
More concisely: If three points in a 2-D real inner product space lie in that order, with the second point strictly between the first and third, then the oriented angle between the first and third points at the second is equal to π.
|
EuclideanGeometry.left_ne_right_of_oangle_sign_eq_neg_one
theorem EuclideanGeometry.left_ne_right_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₁ ≠ p₃
This theorem states that in a 2-dimensional real vector space equipped with an inner product and metric space structure, and with an orientation over a 2-element finite set, if the sign of the oriented angle formed by three points p₁, p₂, and p₃ is -1 (indicating a negative orientation), then the first point p₁ and the third point p₃ cannot be the same. In other words, a negative orientation of the angle between three points in such a space precludes the possibility of the first and third points coinciding.
More concisely: In a 2-dimensional real vector space with an inner product, metric, and orientation over a 2-element set, points with a negative oriented angle cannot be identical.
|
Sbtw.oangle₁₃₂_eq_zero
theorem Sbtw.oangle₁₃₂_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₃ p₂ = 0
This theorem states that for a 2-dimensional real vector space with an orientation, given three points such that the second point is strictly between the first and the third, the oriented angle at the third point (when considered in reverse order) is zero. In other words, if point `p₂` is strictly between point `p₁` and point `p₃`, then the oriented angle from `p₁` to `p₃` via `p₂` is zero. This is a statement in the context of Euclidean Geometry and relates the concept of 'strictly between' with the orientation of angles.
More concisely: In a 2-dimensional real vector space with an orientation, the oriented angle from point `p₁` to point `p₃` via point `p₂` is zero if and only if `p₂` is strictly between `p₁` and `p₃`.
|
Wbtw.oangle₂₁₃_eq_zero
theorem Wbtw.oangle₂₁₃_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₁ p₃ = 0
This theorem states that for a vector space `V` with an inner product over the real numbers ℝ, that is associated to a metric space `P` and is of finite rank 2, if a point `p₂` is weakly between two other points `p₁` and `p₃` (i.e., `p₂` lies on the line segment joining `p₁` and `p₃`), then the oriented angle formed at the first point `p₁` by the three points is zero. This means the three points are co-linear with `p₂` in between `p₁` and `p₃`. The theorem is applicable under the condition that the vector space is oriented.
More concisely: For an oriented finite-rank 2 real inner-product vector space with associated metric space, if point `p₂` lies on the line segment between `p₁` and `p₃`, then the oriented angle formed at `p₁` by the three points is zero, implying they are collinear.
|
EuclideanGeometry.oangle_sub_right
theorem EuclideanGeometry.oangle_sub_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ p₃ : P},
p₁ ≠ p →
p₂ ≠ p →
p₃ ≠ p →
EuclideanGeometry.oangle p₁ p p₃ - EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₂
This theorem is a statement about Euclidean Geometry. It says that given a normed additively commutative group `V`, an inner product space `V` over the real numbers, a metric space `P`, a normed additive torsor `V` over `P`, and given that `V` is a 2-dimensional oriented `ℝ`-module, for any four distinct points `p`, `p₁`, `p₂`, and `p₃` in `P`, the angle at point `p` between `p₁` and `p₃` minus the angle at `p` between `p₂` and `p₃` equals the angle at `p` between `p₁` and `p₂`. This is a generalization of the well-known fact in plane geometry that the difference of two angles at a point equals the third angle.
More concisely: Given a 2-dimensional oriented real inner product space `V` over a metric space `P`, for any four distinct points `p`, `p₁`, `p₂`, and `p₃` in `P`, the angle difference between `p₁` and `p₃`, and the angle difference between `p₂` and `p₃` at point `p` is equal.
|
EuclideanGeometry.oangle_swap₂₃_sign
theorem EuclideanGeometry.oangle_swap₂₃_sign :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
-(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
This theorem states that in a 2-dimensional Euclidean geometry, if you have three points `p₁`, `p₂`, and `p₃` forming an oriented angle, then swapping the position of points `p₂` and `p₃` effectively negates the sign of the original angle. In other words, if the directed or oriented angle from `p₁` to `p₂` to `p₃` has a certain sign (positive or negative, indicating the direction of rotation), then the directed angle from `p₁` to `p₃` to `p₂` will have the opposite sign. Note that the vectors being compared are defined in a real inner product space with a supplied orientation.
More concisely: In a 2-dimensional Euclidean geometry, the signed angle from point `p₁` to point `p₂` to point `p₃` has the opposite sign as the signed angle from point `p₁` to point `p₃` to point `p₂`.
|
EuclideanGeometry.left_ne_right_of_oangle_sign_eq_one
theorem EuclideanGeometry.left_ne_right_of_oangle_sign_eq_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₁ ≠ p₃
This theorem from Euclidean geometry states that if the sign of the oriented angle between three points is positive, then the first and third points are not the same. This is valid in a 2-dimensional real inner product space in which the vector space is endowed with an orientation. The oriented angle is calculated using the three points in the order specified. If its sign is 1 (positive), then it guarantees that the first point and the third point are distinct.
More concisely: In a 2-dimensional real inner product space with an orientation, if the oriented angle between three distinct points is positive, then the first and third points are distinct.
|
AffineSubspace.SSameSide.oangle_sign_eq
theorem AffineSubspace.SSameSide.oangle_sign_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P},
p₁ ∈ s →
p₂ ∈ s →
s.SSameSide p₃ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₃ p₂).sign
This theorem states that given an affine subspace in a two-dimensional real inner product space, if we have four points where the first two points are in the subspace and the other two are on the same side of the subspace, then the angles formed at the first two points by the last two points have the same sign. Here, the angle is calculated using the function `EuclideanGeometry.oangle`, and "having the same sign" refers to the sign of this calculated angle, which is calculated using the `.sign` function.
More concisely: In a two-dimensional real inner product space, if two points lie on an affine subspace and the other two points are on the same side, then the angles formed by the subspace at these two points have the same sign.
|
EuclideanGeometry.left_ne_right_of_oangle_eq_neg_pi_div_two
theorem EuclideanGeometry.left_ne_right_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₁ ≠ p₃
This theorem states that in a 2-dimensional orientable inner product space over the reals, if the oriented angle between three points is `-π / 2`, then the first and third points are not the same. Here, the oriented angle is defined in the sense of Euclidean geometry, and the dimension of the space is ensured to be 2 by the hypothesis that the finite rank of the space (which is set to 0 for infinite-dimensional spaces) is 2.
More concisely: In a 2-dimensional oriented inner product space over the reals, if the oriented angle between two distinct points is `-π / 2`, then the points are not the same.
|
EuclideanGeometry.angle_eq_iff_oangle_eq_of_sign_eq
theorem EuclideanGeometry.angle_eq_iff_oangle_eq_of_sign_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
p₁ ≠ p₂ →
p₃ ≠ p₂ →
p₄ ≠ p₅ →
p₆ ≠ p₅ →
(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign →
(EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ ↔
EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆)
This theorem states that for a 2-dimensional vector space `V` over the real numbers with a given orientation and six distinct points `p₁`, `p₂`, `p₃`, `p₄`, `p₅`, and `p₆` in a metric space `P` equipped with a normed add torsor structure over `V`. If the signs of the oriented angles formed by `p₁`, `p₂`, `p₃` and `p₄`, `p₅`, `p₆` are equal, then the non-oriented angles between the points `p₁`, `p₂`, `p₃` and `p₄`, `p₅`, `p₆` are equal if and only if the oriented angles between these points are equal.
More concisely: Given a 2-dimensional real vector space `V` with orientation, and six distinct points `p₁, p₂, p₃, p₄, p₅, p₆` in a metric space `P` with a normed add torsor structure over `V`, the non-oriented angles between `p₁, p₂, p₃` and `p₄, p₅, p₆` are equal if and only if their oriented angles are equal when the signs of the oriented angles formed by adjacent points are equal.
|
Wbtw.oangle₂₃₁_eq_zero
theorem Wbtw.oangle₂₃₁_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₃ p₁ = 0
This theorem states that in a two-dimensional oriented module over the real numbers, given three points where the second point is weakly between the first and third points, the oriented angle at the third point with respect to the first and second points is zero. In other words, if you have three points and the middle point lies on the line segment between the other two, then the angle created at the third point by lines to the first and second points is zero. This theorem holds in the context of an inner product space with a metric space and normed add torsor structures.
More concisely: In a two-dimensional oriented real module, the angle between the vectors formed by lines from the first to the second and from the first to the third points is zero, given that the second point lies on the line segment between the first and third points.
|
EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero
theorem EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P},
(EuclideanGeometry.oangle p₁ p p₂).sign = 0 →
p₁ = p ∨ p₂ = p ∨ EuclideanGeometry.angle p₁ p p₂ = 0 ∨ EuclideanGeometry.angle p₁ p p₂ = Real.pi
This theorem states that in a two-dimensional oriented module over the real numbers, given three points `p`, `p₁`, and `p₂`, if the sign of the oriented angle at `p` between `p₁` and `p₂` is zero, it implies one of the following conditions: either `p₁` equals `p`, `p₂` equals `p`, the unoriented angle between `p₁` and `p₂` at `p` is zero, or the unoriented angle between `p₁` and `p₂` at `p` is π (pi).
More concisely: In a two-dimensional oriented real module, if the signed angle between vectors `p₁-p` and `p₂-p` is zero, then either `p₁ = p`, `p₂ = p`, or the unoriented angle between `p₁-p` and `p₂-p` is π.
|
Wbtw.oangle₃₁₂_eq_zero
theorem Wbtw.oangle₃₁₂_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₁ p₂ = 0
The theorem `Wbtw.oangle₃₁₂_eq_zero` states that for any three points `p₁`, `p₂`, and `p₃` in a two-dimensional, oriented vector space (with an inner product space structure over the reals), if `p₂` is weakly between `p₁` and `p₃` (as defined by the `Wbtw` function), then the oriented angle at `p₁` (when the order of the points is reversed, i.e., considered as `p₃`, `p₁`, `p₂`) is zero. This means that, geometrically, `p₁`, `p₂`, and `p₃` form a straight line.
More concisely: If three points `p₁`, `p₂`, `p₃` in a 2-dimensional, oriented real vector space with an inner product form a weakly between relation, then the oriented angle between `p₁` and `p₃` with `p₂` as the vertex is zero.
|
EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle
theorem EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P},
p₁ ≠ p →
p₂ ≠ p →
EuclideanGeometry.oangle p₁ p p₂ = ↑(EuclideanGeometry.angle p₁ p p₂) ∨
EuclideanGeometry.oangle p₁ p p₂ = -↑(EuclideanGeometry.angle p₁ p p₂)
This theorem states that the oriented angle at a point `p` between two other points `p₁` and `p₂` (neither of which is equal to `p`) is either equal to the unoriented angle or its negative. This is made precise in a Euclidean geometry context, where `V` is a normed add commutative group and `P` is a metric space. We also require `V` to be an inner product space over the real numbers `ℝ`, `P` to be a normed add torsor over `V`, and `V` to have a dimension of two with an orientation structure. The orientation structure on `V` makes the notion of an "oriented angle" well-defined.
More concisely: In a Euclidean geometry context where $V$ is a two-dimensional oriented inner product space with a metric space structure $P$, the oriented angle at point $p$ between vectors $p\_1 - p$ and $p\_2 - p$ is equal to or the negative of the unoriented angle between $p\_1$ and $p\_2$.
|
Sbtw.oangle_eq_add_pi_right
theorem Sbtw.oangle_eq_add_pi_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₃' : P},
Sbtw ℝ p₃ p₂ p₃' → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃' + ↑Real.pi
This theorem, `Sbtw.oangle_eq_add_pi_right`, states that in a 2-dimensional oriented normed vector space over the real numbers, given four points `p₁`, `p₂`, `p₃`, and `p₃'`, if `p₂` is strictly between `p₃` and `p₃'`, and `p₁` is not equal to `p₂`, then the oriented angle from `p₁` to `p₂` to `p₃` is equal to the oriented angle from `p₁` to `p₂` to `p₃'` plus π radians. This means that replacing the third point `p₃` by a point `p₃'` on the same line but the opposite ray adds π to the oriented angle.
More concisely: In a 2-dimensional oriented normed vector space over the real numbers, the angle from a point to two points on the same line but opposite rays differs by π radians.
|
Sbtw.oangle_sign_eq_right
theorem Sbtw.oangle_sign_eq_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (p₄ : P),
Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
This theorem states that for any set of four points where three of them are strictly in order on the same line, the angles formed at the fourth point between the second and third or first and third points have the same sign. This is under the condition that the underlying vector space is a normed additative commutative group with real inner product, the set of points is a metric space, the torsor structure over the vector space is normed and additive, the vector space is two dimensional, and the orientation of the vector space is given by the standard orientation.
More concisely: If three points on a line in a two-dimensional real normed vector space with standard orientation form a strictly increasing order, then the angles formed between the lines connecting the fourth point to the second and third points have the same sign.
|
EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq
theorem EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆ →
(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign →
EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆
The theorem `EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq` states that in a 2-dimensional Euclidean space, if two unoriented angles (defined by three points each) are equal, and the signs of the corresponding oriented angles are the same, then the oriented angles themselves are also equal. This holds true even in degenerate cases where some of the points coincide. In the mathematical notation, if the unoriented angles `p₁p₂p₃` and `p₄p₅p₆` are equal, and the signs of the oriented angles `p₁p₂p₃` and `p₄p₅p₆` are equal, then the oriented angles `p₁p₂p₃` and `p₄p₅p₆` are equal.
More concisely: In a 2-dimensional Euclidean space, if two unoriented angles are equal and have the same orientation, then their oriented angles are equal.
|
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
This theorem states that in a 2-dimensional Euclidean space defined over the real numbers, if the oriented angle between three points (`p₁`, `p₂`, `p₃`) is `π / 2` (or 90 degrees), then the unoriented angle when the points are reversed (i.e., `p₃`, `p₂`, `p₁`) is also `π / 2`. An oriented angle takes into account the rotation direction from one line to another, while an unoriented angle only considers the smallest angle between the two lines, regardless of rotation direction.
More concisely: In a 2-dimensional Euclidean space over the real numbers, the oriented angle between three points is equal to the oriented angle when the points are reversed if and only if the angle is a right angle (90 degrees).
|
EuclideanGeometry.right_ne_of_oangle_sign_eq_neg_one
theorem EuclideanGeometry.right_ne_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₃ ≠ p₂
The theorem `EuclideanGeometry.right_ne_of_oangle_sign_eq_neg_one` states that in a 2-dimensional oriented normed vector space over the real numbers, given any three points `p₁`, `p₂` and `p₃`, if the sign of the oriented angle between these points is `-1`, which indicates a "negative" orientation, then the last two points `p₃` and `p₂` cannot be equal. Here, the oriented angle is a concept from Euclidean geometry that measures the counterclockwise angle from the positive x-axis to the line segment connecting the first two points, oriented towards the third point.
More concisely: In a 2-dimensional oriented normed vector space over the real numbers, if the oriented angle between points `p₁`, `p₂`, and `p₃` is `-1` radians, then `p₂` and `p₃` are not equal.
|
EuclideanGeometry.oangle_midpoint_left
theorem EuclideanGeometry.oangle_midpoint_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle (midpoint ℝ p₁ p₂) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃
This theorem states that in a 2-dimensional Euclidean space, the oriented angle defined by three points is not changed if the first point is replaced with the midpoint of the segment between the first and the second point. In other words, if you have three points `p₁`, `p₂`, and `p₃`, the oriented angle at `p₂` formed by the points `midpoint ℝ p₁ p₂`, `p₂`, and `p₃` is the same as the oriented angle formed by the points `p₁`, `p₂`, and `p₃`. The space is assumed to be equipped with a normed add commutative group structure, an inner product space over the reals, a metric space structure, and a normed add torsor structure. The vector space of the underlying geometry is assumed to have an orientation.
More concisely: In a 2-dimensional Euclidean space with an orientation, the oriented angle between two line segments with a common endpoint is invariant under replacement of one endpoint with the midpoint of the segment.
|
EuclideanGeometry.oangle_midpoint_right
theorem EuclideanGeometry.oangle_midpoint_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle p₁ p₂ (midpoint ℝ p₃ p₂) = EuclideanGeometry.oangle p₁ p₂ p₃
This theorem in Euclidean Geometry states that the oriented angle determined by three points (p₁, p₂, p₃) remains the same if the third point (p₃) is replaced by the midpoint of the line segment between p₃ and the second point (p₂). This statement holds true for a normed add commutative group V, with an inner product space over the real numbers, ℝ, and a metric space P, where V is the normed add torsor for P. Additionally, it assumes that the finite rank of V over ℝ is 2 and that V is a ℝ-oriented module with a dimension of 2.
More concisely: In a 2-dimensional Euclidean space with inner product and metric, the orientation of the angle between two vectors, represented as line segments with endpoints p₁, p₂, and p₃ (with p₃ on the line segment between p₁ and p₂), remains constant.
|
Sbtw.oangle_eq_left_right
theorem Sbtw.oangle_eq_left_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₁' p₂ p₃ p₃' : P},
Sbtw ℝ p₁ p₂ p₁' → Sbtw ℝ p₃ p₂ p₃' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃'
This theorem states that in a 2-dimensional Euclidean space, if you have three points `p₁`, `p₂`, and `p₃`, and you replace `p₁` and `p₃` with `p₁'` and `p₃'` such that `p₂` is strictly between `p₁` and `p₁'` and also strictly between `p₃` and `p₃'`, then the oriented angle between the vectors `p₁p₂` and `p₂p₃` equals the oriented angle between the vectors `p₁'p₂` and `p₂p₃'`. This means that the change of points doesn't affect the oriented angle, which is essentially the concept of vertically opposite angles.
More concisely: In a 2-dimensional Euclidean space, if points `p₁`, `p₂`, `p₃` and `p₁'`, `p₂`, `p₃'` are such that `p₂` is strictly between `p₁` and `p₁'`, and `p₂` is strictly between `p₃` and `p₃'`, then the oriented angle between `p₁p₂` and `p₂p₃` equals the oriented angle between `p₁'p₂` and `p₂p₃'`.
|
EuclideanGeometry.oangle_add_cyc3
theorem EuclideanGeometry.oangle_add_cyc3 :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ p₃ : P},
p₁ ≠ p →
p₂ ≠ p →
p₃ ≠ p →
EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₃ p p₁ =
0
This theorem, known as `EuclideanGeometry.oangle_add_cyc3`, states that given a normed add commutative group `V`, a metric space `P`, an inner product space with real numbers on `V`, and a Normed Additive Torsor over `V` and `P` with the condition that `V` is two-dimensional and oriented, for any four distinct points `p`, `p₁`, `p₂` and `p₃` in `P` where `p₁`, `p₂`, and `p₃` are not equal to `p`, the sum of the angles at `p` between `p₁` and `p₂`, `p₂` and `p₃`, and `p₃` and `p₁`, taken in cyclic order, is equal to zero. This is equivalent to the geometrical fact in Euclidean geometry that the sum of the internal angles of a triangle is 180 degrees, since each angle in Lean is represented in radians, and 180 degrees equals to π radians which is equivalent to 0 in the cycle group of real numbers by 2π.
More concisely: In a two-dimensional, oriented Normed Additive Torsor over a normed additive group and metric space with an inner product of real numbers, the sum of the angles between any three distinct points taken in cyclic order is equivalent to 0 in the cycle group of real numbers, which represents the geometrical fact that the sum of the interior angles of a triangle equals 180 degrees in Euclidean geometry.
|
EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq
theorem EuclideanGeometry.oangle_eq_pi_sub_two_zsmul_oangle_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
p₂ ≠ p₃ →
dist p₁ p₂ = dist p₁ p₃ →
EuclideanGeometry.oangle p₃ p₁ p₂ = ↑Real.pi - 2 • EuclideanGeometry.oangle p₁ p₂ p₃
This theorem states that in Euclidean geometry, if we have a normed additive commutative group `V`, an inner product space over the real numbers within `V`, a metric space `P`, and a normed additive torsor over `V` and `P`. Moreover, if the rank of the module `V` over the real numbers is 2 and this module is oriented, and we have three distinct points `p₁`, `p₂`, `p₃` in `P` such that `p₂` is not equal to `p₃` and the distances from `p₁` to `p₂` and `p₁` to `p₃` are equal (that is, the triangle formed by `p₁`, `p₂`, `p₃` is isosceles), then the oriented angle at `p₁` (the apex of the isosceles triangle) is equal to π (the mathematical constant representing the ratio of a circle's circumference to its diameter) minus twice the oriented angle at `p₂` (a base angle of the isosceles triangle).
More concisely: In Euclidean geometry, if `V` is a 2-dimensional real oriented normed additive group, `P` is a metric space, `p₁`, `p₂`, `p₃` are distinct points in `P` forming an isosceles triangle with equal sides, then the oriented angle at `p₁` is equal to π - 2 * oriented angle at `p₂`.
|
EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq
theorem EuclideanGeometry.affineIndependent_iff_of_two_zsmul_oangle_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆ →
(AffineIndependent ℝ ![p₁, p₂, p₃] ↔ AffineIndependent ℝ ![p₄, p₅, p₆])
This theorem in Euclidean Geometry states that, given two sets of three points, p₁, p₂, p₃ and p₄, p₅, p₆, in a real inner product space of finite rank 2, if twice the oriented angle between the first set of points equals twice the oriented angle between the second set of points, then the first set of points is affinely independent if and only if the second set of points is. Affine independence here is defined as no nontrivial weighted subtractions (where the sum of weights is 0) being 0.
More concisely: In a real inner product space of finite rank 2, if the oriented angle between set {p₁, p₂, p₃} is twice that of set {p₄, p₅, p₆}, then both sets are affine independent if and only if no weighted sum of distinct points from either set with sum of weights equal to zero is zero.
|
EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq
theorem EuclideanGeometry.two_zsmul_oangle_of_vectorSpan_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
vectorSpan ℝ {p₁, p₂} = vectorSpan ℝ {p₄, p₅} →
vectorSpan ℝ {p₃, p₂} = vectorSpan ℝ {p₆, p₅} →
2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆
This theorem from Euclidean Geometry states that if we have two pairs of points such that the vector span of the first pair equals the vector span of the second pair, and similarly for another two pairs of points, then the double of the angle formed by the first three points equals the double of the angle formed by the second three points. This is under the condition that the points come from a metric space and the vector space they come from has exactly 2 dimensions over the field of real numbers, and that the vector space is equipped with an inner product and a norm, and it has a specific orientation.
More concisely: If two sets of three points in a 2-dimensional Euclidean space with an inner product and norm over the real numbers have the same span and the same orientation, then they form congruent angles.
|
EuclideanGeometry.left_ne_of_oangle_eq_neg_pi_div_two
theorem EuclideanGeometry.left_ne_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₁ ≠ p₂
This theorem, from the field of Euclidean Geometry, states that if the oriented angle (counter-clockwise from the positive x-axis) between three points is `-π / 2` radians (or `-90` degrees), then the first two points cannot be equal. The theorem is applicable in the context of a 2-dimensional real inner product space, where the points are elements of a metric space and vectors are elements of a normed additively commutative group. The orientation of the space is given by a choice of ordered basis (in this case, a basis with two elements), which is part of the definition of an oriented module over the real numbers.
More concisely: In a 2-dimensional real inner product space with an oriented basis, if the oriented angle between any two distinct points is -π/2 radians (or -90 degrees), then the points are not equal.
|
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two
theorem EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
This theorem states that in a 2-dimensional oriented module `V` over the field of real numbers `ℝ`, if the oriented angle (`EuclideanGeometry.oangle`) between three points `p₁`, `p₂`, and `p₃` is `-π / 2`, then the unoriented angle (`EuclideanGeometry.angle`) formed when the points are reversed (i.e., `p₃`, `p₂`, `p₁` instead of `p₁`, `p₂`, `p₃`) is `π / 2`. The notion of an "oriented" angle takes into account the order of the points, unlike the "unoriented" angle.
More concisely: In a 2-dimensional oriented real vector space, the oriented angle between three points is `-π/2` if and only if the unoriented angle formed by the reversed order of these points is `π/2`.
|
EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one
theorem EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
(EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 →
EuclideanGeometry.oangle p₁ p₂ p₃ = -↑(EuclideanGeometry.angle p₁ p₂ p₃)
The theorem `EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one` states that, given a 2-dimensional vector space `V` over the real numbers, and three points `p₁`, `p₂`, and `p₃` in a normed add-torsor over `V` (which can be thought of as an affine space), if the sign of the oriented angle between these three points is `-1`, then the oriented angle equals the negative of the unoriented angle between the three points. In other words, if the oriented angle is measured in the opposite direction, its value is the negative of the unoriented angle.
More concisely: If the oriented angle between three points in a 2-dimensional vector space over the real numbers is -1 times the unoriented angle, then the oriented angle equals the negative of the unoriented angle.
|
EuclideanGeometry.right_ne_of_oangle_sign_ne_zero
theorem EuclideanGeometry.right_ne_of_oangle_sign_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₃ ≠ p₂
The theorem states that in a Euclidean geometry context, if the sign of the oriented angle formed by three points is non-zero, then the third and second points cannot be the same. This theorem is applicable in a specific mathematical setting where the underlying vector space is a normed add commutative group with an inner product space structure over the real numbers, and the point set is a metric space with normed add torsor structure. The theorem also assumes that the space is two-dimensional and oriented.
More concisely: In a two-dimensional Euclidean geometry setting with an oriented inner product space structure over the real numbers, distinct points form a non-zero angle.
|
EuclideanGeometry.oangle_eq_angle_of_sign_eq_one
theorem EuclideanGeometry.oangle_eq_angle_of_sign_eq_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
(EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 →
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(EuclideanGeometry.angle p₁ p₂ p₃)
The theorem `EuclideanGeometry.oangle_eq_angle_of_sign_eq_one` states that for a vector space `V` with a finite rank of 2 over the real numbers `ℝ` and a set of points `P` in `V`, if the oriented angle (denoted by `EuclideanGeometry.oangle`) between three points `p₁`, `p₂` and `p₃` has a sign of 1 (indicating that the angle is strictly between `0` and `π`), then this oriented angle is equal to the unoriented angle (denoted by `EuclideanGeometry.angle`) between the same three points.
More concisely: If the oriented angle between three points in a 2-dimensional real vector space has a positive sign, then it is equal to the unoriented angle between the same three points.
|
Collinear.two_zsmul_oangle_eq_left
theorem Collinear.two_zsmul_oangle_eq_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₁' p₂ p₃ : P},
Collinear ℝ {p₁, p₂, p₁'} →
p₁ ≠ p₂ → p₁' ≠ p₂ → 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁' p₂ p₃
This theorem states that for a given normed additive commutative group `V`, an inner product space over `V` with real numbers, a metric space `P`, a normed additive torsor over `V` and `P`, and an orientation over `V` with real numbers, if the finite rank of `V` over real numbers is `2`, then for any four points `p₁`, `p₁'`, `p₂`, and `p₃`, if `p₁`, `p₂`, and `p₁'` are collinear and `p₁` is not equal to `p₂` and `p₁'` is not equal to `p₂`, then twice the oriented angle between `p₁`, `p₂`, and `p₃` is equal to twice the oriented angle between `p₁'`, `p₂`, and `p₃`. In simpler terms, replacing the first point of a triangle by another point on the same line does not change twice the measure of the oriented angle made by the three points of the triangle.
More concisely: For a 2-dimensional real vector space `V` with inner product, given collinear points `p₁`, `p₂`, `p₃` and `p'_i` (not equal to `p_i`), the twice-signed angle between `(p'_1, p'_2)` and `(p_2, p_3)` is equal to the twice-signed angle between `(p_1, p_2)` and `(p_2, p_3)`.
|
EuclideanGeometry.continuousAt_oangle
theorem EuclideanGeometry.continuousAt_oangle :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {x : P × P × P},
x.1 ≠ x.2.1 → x.2.2 ≠ x.2.1 → ContinuousAt (fun y => EuclideanGeometry.oangle y.1 y.2.1 y.2.2) x
This theorem is stating that oriented angles in a Euclidean plane are continuous whenever the two end points do not coincide with the middle point. In more detail, it asserts that for any triple of points in a 2-dimensional real inner product space (which we think of as Euclidean space), provided that the first point does not equal the second and the third point does not equal the second, the function that takes a triple of points to the oriented angle they form is continuous at that triple. This means that a small movement of any of the points will result in a small change in the angle.
More concisely: The function that maps a triple of distinct points in a 2-dimensional Euclidean space to the oriented angle they form is continuous.
|
Sbtw.oangle_eq_right
theorem Sbtw.oangle_eq_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₃' : P},
Sbtw ℝ p₂ p₃ p₃' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'
This theorem states that in a 2-dimensional real inner product space, given four points `p₁`, `p₂`, `p₃`, `p₃'` such that `p₃` is strictly between `p₂` and `p₃'`, the oriented angle formed by `p₁`, `p₂`, and `p₃` is equal to the oriented angle formed by `p₁`, `p₂`, and `p₃'`. In other words, the oriented angle at `p₂` doesn't change if `p₃` is replaced by `p₃'`, which is further away on the same ray as `p₃`.
More concisely: In a 2-dimensional real inner product space, if points `p₂`, `p₃`, and `p₃'` form a strictly increasing chain, then the oriented angles formed by `p₁`, `p₂`, and `p₃`, and `p₁`, `p₂`, and `p₃'` are equal.
|
EuclideanGeometry.oangle_eq_pi_iff_sbtw
theorem EuclideanGeometry.oangle_eq_pi_iff_sbtw :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Sbtw ℝ p₁ p₂ p₃
This theorem is about a geometric property in a 2-dimensional Euclidean space. It states that for a given space with an oriented inner product (where the space is a metric space, and it is also a torsor space over a normed additively commutative group), the oriented angle among three points (p₁, p₂, p₃) is equal to π if and only if the second point (p₂) is strictly between the other two points (p₁ and p₃). Here, "strictly between" means that p₂ is between p₁ and p₃, but is not equal to either of them. The dimension of the space is assumed to be 2.
More concisely: In a 2-dimensional Euclidean space with an oriented inner product, the oriented angle between three points is equal to π if and only if the second point is strictly between the other two.
|
Sbtw.oangle₁₂₃_eq_pi
theorem Sbtw.oangle₁₂₃_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi
This theorem states that if the second of three points in a two-dimensional oriented inner product space over the reals is strictly between the other two, then the oriented angle at that second point is equal to π. The vector space is assumed to be normed, and the points are assumed to form a metric space with the normed add-torsor structure. The oriented angle function, `EuclideanGeometry.oangle`, returns an angle in radians between 0 and 2π, and it is proven here to return π under the specified conditions.
More concisely: If three points in a 2-dimensional real normed inner product space form an acute angle greater than 90 degrees with the second point being the vertex, then the oriented angle between the first and third points is equal to π radians.
|
EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq
theorem EuclideanGeometry.abs_oangle_left_toReal_lt_pi_div_two_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
dist p₁ p₂ = dist p₁ p₃ → |(EuclideanGeometry.oangle p₂ p₃ p₁).toReal| < Real.pi / 2
This theorem states that in a Euclidean Geometry, if we consider an isosceles triangle with vertices labeled as `p₁`, `p₂`, and `p₃`, where the distance between `p₁` and `p₂` is equal to the distance between `p₁` and `p₃`, then the absolute value of the oriented angle at `p₁` (measured in radians) is less than π/2. Here, the space in which the points are defined is a 2-dimensional real vector space equipped with an inner product and a specified orientation.
More concisely: In Euclidean geometry, an isosceles triangle with vertex labels `p₁`, `p₂`, and `p₃` having equal side lengths `|vp₂ - vp₁| = |vp₃ - vp₁|` has the absolute value of the angle at `p₁` (measured in radians) less than π/2.
|
EuclideanGeometry.left_ne_of_oangle_eq_pi
theorem EuclideanGeometry.left_ne_of_oangle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi → p₁ ≠ p₂
This theorem, from Euclidean Geometry, states that if the angle formed by three points is equal to `π` (pi, the ratio of the circumference of a circle to its diameter, approximately 3.14159), then the first two points are distinct, they cannot be the same. This holds in a two-dimensional vector space over the real numbers, with standard inner product and metric space structures, and is coupled with the assumption that the space is oriented. The angle between the points is defined by the Euclidean Geometry's `oangle` function.
More concisely: In a two-dimensional real vector space with standard inner product and metric space structures, and under the assumption of orientation, the angle between two distinct points is not equal to pi.
|
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
This theorem states that if the oriented angle between three points is `π / 2`, then the unoriented angle between these points is also `π / 2`. Here, the oriented angle is defined in the context of a 2-dimensional vector space over the real numbers, equipped with an orientation and standard Euclidean geometry. The points are taken in a metric space with a normed add torsor structure, which is a space where you can add vectors to points and subtract points to get vectors.
More concisely: In a 2-dimensional real vector space with orientation and standard Euclidean geometry, the unoriented angle between three points is `π / 2` if and only if their oriented angle is `π / 2`.
|
Wbtw.oangle_sign_eq_of_ne_left
theorem Wbtw.oangle_sign_eq_of_ne_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (p₄ : P),
Wbtw ℝ p₁ p₂ p₃ → p₁ ≠ p₂ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
This theorem states that given four points `p₁`, `p₂`, `p₃`, and `p₄` in a two-dimensional real vector space, where `p₁`, `p₂`, and `p₃` are in weak order on the same line and `p₁` is not equal to `p₂`, the sign of the angle at `p₄` between `p₁` and `p₂` is the same as the sign of the angle at `p₄` between `p₁` and `p₃`. This means if we're looking from `p₄`, the relative direction to move towards `p₁` from `p₂` and `p₃` is the same.
More concisely: Given three collinear points `p₁`, `p₂`, `p₃` in a 2-dimensional real vector space with `p₁` neither equal to `p₂`, the signed angle between `p₁` and `p₂` is equal to the signed angle between `p₁` and `p₃`.
|
EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero
theorem EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P},
p₁ ≠ p → p₂ ≠ p → (EuclideanGeometry.oangle p₁ p p₂ = 0 ↔ EuclideanGeometry.angle p₁ p p₂ = 0)
This theorem states that, in a two-dimensional oriented module over the real numbers, the unoriented angle at a point `p` between two other points `p₁` and `p₂` (none of which are equal to `p`) is zero if and only if the oriented angle at `p` between `p₁` and `p₂` is also zero. This assertion holds in the context of Euclidean Geometry where the vector space `V` has a normed additive commutative group structure, an inner product space structure over the real numbers, and the point space `P` has a metric space structure. The theorem essentially relates the equality to zero of the unoriented and oriented angles between two distinct points with respect to a third point.
More concisely: In a two-dimensional oriented module over the real numbers with Euclidean geometry structure, the unoriented angle between two distinct points is zero if and only if their oriented angle is zero at a given point.
|
EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi
theorem EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
This theorem states that, for three points in a 2-dimensional real vector space (or equivalently, on the plane), the oriented angle between the three points is equal to pi (or equivalently, 180 degrees) if and only if the unoriented angle between them is also equal to pi. Here, the oriented angle incorporates a notion of direction (clockwise or counterclockwise), whereas the unoriented angle simply measures the smallest angle between the lines, without considering direction. Note that by "angle between three points", we mean the angle formed at the middle point by lines drawn to the other two points.
More concisely: In a 2-dimensional real vector space, the oriented angle is pi (180 degrees) between three points if and only if their unoriented angle is also pi.
|
EuclideanGeometry.angle_eq_abs_oangle_toReal
theorem EuclideanGeometry.angle_eq_abs_oangle_toReal :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P},
p₁ ≠ p → p₂ ≠ p → EuclideanGeometry.angle p₁ p p₂ = |(EuclideanGeometry.oangle p₁ p p₂).toReal|
This theorem states that in a 2-dimensional oriented Euclidean space, for any three distinct points `p`, `p₁`, and `p₂`, the unoriented angle at `p` between `p₁` and `p₂` is equal to the absolute value of the oriented angle between them. In other words, when we disregard the direction of rotation, the measure of the angle between two points not equal to `p` is given by the absolute value of the measure of the corresponding oriented angle.
More concisely: In a 2-dimensional oriented Euclidean space, the absolute value of the oriented angle between any two distinct points equals the unoriented angle between them.
|
EuclideanGeometry.oangle_self_left
theorem EuclideanGeometry.oangle_self_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₁ p₂ = 0
This theorem, named `EuclideanGeometry.oangle_self_left`, states that for any given `NormedAddCommGroup` V and `InnerProductSpace` over the real numbers ℝ in V, along with a `MetricSpace` P and a `NormedAddTorsor` V P, if V has a `FiniteDimensional.finrank` of 2 and is oriented, then the Euclidean angle ∡AAB at a point, where A is the point itself and B is another point, is always equal to 0. In other words, the angle between a vector from a point to itself and a vector from this point to another point is 0.
More concisely: For any 2-dimensional, oriented Normed Add Comm Group V over the real numbers with an Inner Product Space structure and a Normed Add Torsor over a Metric Space P, the Euclidean angle between vectors from a point to itself and from that point to another point is equal to 0.
|
EuclideanGeometry.two_zsmul_oangle_of_parallel
theorem EuclideanGeometry.two_zsmul_oangle_of_parallel :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P},
(affineSpan ℝ {p₁, p₂}).Parallel (affineSpan ℝ {p₄, p₅}) →
(affineSpan ℝ {p₃, p₂}).Parallel (affineSpan ℝ {p₆, p₅}) →
2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆
The theorem `EuclideanGeometry.two_zsmul_oangle_of_parallel` states that in a two-dimensional oriented Euclidean geometry, given six points `p₁`, `p₂`, `p₃`, `p₄`, `p₅`, and `p₆`, if the lines determined by the pairs of points `(p₁, p₂)` and `(p₄, p₅)` are parallel, and the lines determined by the pairs `(p₃, p₂)` and `(p₆, p₅)` are also parallel, then twice the angle formed by `p₁`, `p₂`, and `p₃` equals twice the angle formed by `p₄`, `p₅`, and `p₆`. Here, the angle is measured using the Euclidean geometry's inner product space convention and the lines are defined as the smallest affine subspaces containing the respective pairs of points.
More concisely: In a two-dimensional oriented Euclidean geometry, if lines determined by pairs of points (p₁, p₂) and (p₄, p₅), as well as pairs (p₃, p₂) and (p₆, p₅), are parallel, then twice the angle formed by points p₁, p₂, and p₃ equals twice the angle formed by points p₄, p₅, and p₆.
|
Sbtw.oangle_eq_left
theorem Sbtw.oangle_eq_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₁' p₂ p₃ : P},
Sbtw ℝ p₂ p₁ p₁' → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃
The theorem `Sbtw.oangle_eq_left` states that for any points `p₁`, `p₁'`, `p₂`, and `p₃` in an oriented two-dimensional real inner product space `V` (a plane), if `p₁` is strictly between `p₂` and `p₁'` (`p₂`, `p₁`, `p₁'` are in that order on a line), then the oriented angle `p₁ p₂ p₃` (the angle from `p₂` to `p₃` as viewed from `p₁`) is the same as the oriented angle `p₁' p₂ p₃` (the angle from `p₂` to `p₃` as viewed from `p₁'`). In simpler terms, moving the point of observation along the ray from `p₂` through `p₁` does not change the observed angle between `p₂` and `p₃`.
More concisely: If points `p₁`, `p₂`, and `p₃` in an oriented 2-dimensional real inner product space `V` lie on a line with `p₁` strictly between `p₂` and `p₃`, then the oriented angles `p₁p₂p₃` and `p₁'p₂p₃` are equal, where `p₁'` is any point on the ray from `p₂` through `p₁`.
|
EuclideanGeometry.oangle_add_oangle_rev
theorem EuclideanGeometry.oangle_add_oangle_rev :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle p₁ p₂ p₃ + EuclideanGeometry.oangle p₃ p₂ p₁ = 0
This theorem states that in a 2-dimensional oriented vector space over the field of real numbers, if we take any three points, the sum of the oriented angle from the first to the second through the third and the oriented angle from the third to the second through the first is always zero. The space is equipped with norms, inner products, and metrics, and has the structure of a normed add-torsor. The theorem is valid regardless of the specific points chosen.
More concisely: In a 2-dimensional oriented real vector space with norms, inner products, and metrics, the sum of the oriented angles between any three points is always zero.
|
Sbtw.oangle₃₁₂_eq_zero
theorem Sbtw.oangle₃₁₂_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₃ p₁ p₂ = 0
This theorem states that given a vector space `V` with an inner product space over the real numbers `ℝ`, a metric space `P`, a module over `V` with a normed add torsor structure, an orientation on the 2-dimensional module over `V`, and three points `p₁`, `p₂`, and `p₃` in `P`, if the point `p₂` is strictly between `p₁` and `p₃`, then the oriented angle `oangle` at `p₁`, with respect to `p₃` and `p₂`, is zero. This essentially means that if `p₂` lies strictly on the line segment from `p₁` to `p₃`, then the angle between the vectors `p₃-p₁` and `p₂-p₁` is zero, implying that they are co-linear.
More concisely: Given a real inner product space `V`, a normed module `P` over `V` with an orientation, if points `p₁`, `p₂`, and `p₃` in `P` satisfy `p₂` being strictly between `p₁` and `p₃`, then the oriented angle between `p₃ - p₁` and `p₂ - p₁` is zero, implying they are collinear.
|
EuclideanGeometry.cos_oangle_eq_cos_angle
theorem EuclideanGeometry.cos_oangle_eq_cos_angle :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P},
p₁ ≠ p → p₂ ≠ p → (EuclideanGeometry.oangle p₁ p p₂).cos = (EuclideanGeometry.angle p₁ p p₂).cos
This theorem states that for any three distinct points `p`, `p₁`, and `p₂` in a metric space `P`, with the space `P` being a normed add torsor over a normed additive commutative group `V` with an inner product and which is 2-dimensional and oriented over the real numbers, the cosine of the oriented angle at `p` between `p₁` and `p₂` is equal to the cosine of the unoriented angle at `p` between `p₁` and `p₂`. This implies that the orientation of the angle does not affect its cosine value.
More concisely: In a 2-dimensional oriented inner product space over the real numbers, the cosine of the oriented angle between any three distinct points is equal to the cosine of the unoriented angle between them.
|
EuclideanGeometry.oangle_swap₁₃_sign
theorem EuclideanGeometry.oangle_swap₁₃_sign :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
-(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₃ p₂ p₁).sign
The theorem `EuclideanGeometry.oangle_swap₁₃_sign` states that for any three points `p₁`, `p₂`, `p₃` in a 2-dimensional real inner-product space with a given orientation, swapping the first and third points in an oriented angle negates the sign of that angle. In other words, the sign of the oriented angle formed by `p₁`, `p₂`, `p₃` is the negative of the sign of the oriented angle formed by `p₃`, `p₂`, `p₁`. This theorem reflects the geometric intuition that reversing the order of points in an angle effectively mirrors the angle, changing its orientation.
More concisely: The sign of the oriented angle between points `p₁`, `p₂`, and `p₃` in a 2-dimensional real inner-product space is the negative of the sign of the oriented angle between points `p₃`, `p₂`, and `p₁`.
|
Wbtw.oangle_sign_eq_of_ne_right
theorem Wbtw.oangle_sign_eq_of_ne_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (p₄ : P),
Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → (EuclideanGeometry.oangle p₂ p₄ p₃).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
This theorem, `Wbtw.oangle_sign_eq_of_ne_right`, asserts that for a 2-dimensional real vector space, given four points where the first three points are in weak order on the same line with the second point not being equal to the third, the orientations (signs) of the angles at the fourth point between the second and third points or between the first and third points are the same. This means that the viewpoint of the fourth point regarding the other three points doesn't alter the order in which these points appear.
More concisely: Given a 2-dimensional real vector space and three points on a line in weak order, the orientation of the angle at the fourth point between the second and third points is equal to the orientation of the angle at the fourth point between the first and third points.
|
Collinear.two_zsmul_oangle_eq_right
theorem Collinear.two_zsmul_oangle_eq_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₃' : P},
Collinear ℝ {p₃, p₂, p₃'} →
p₃ ≠ p₂ → p₃' ≠ p₂ → 2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃'
The theorem `Collinear.two_zsmul_oangle_eq_right` states that in a two-dimensional oriented Euclidean space with inner product over reals, for any points `p₁`, `p₂`, `p₃` and `p₃'`, if `p₃`, `p₂`, and `p₃'` are collinear and `p₃` and `p₃'` are distinct from `p₂`, then the double of the oriented angle from `p₁` via `p₂` to `p₃` is equal to the double of the oriented angle from `p₁` via `p₂` to `p₃'`. In other words, replacing the third point in an oriented angle by another one on the same line does not change the double of the oriented angle value.
More concisely: In a 2-dimensional oriented Euclidean space with real inner product, if points `p₁`, `p₂`, and distinct points `p₃` and `p₃'` are collinear, then the double of the oriented angle from `p₁` via `p₂` to `p₃` equals the double of the oriented angle from `p₁` via `p₂` to `p₃'`.
|
EuclideanGeometry.left_ne_of_oangle_sign_eq_one
theorem EuclideanGeometry.left_ne_of_oangle_sign_eq_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₁ ≠ p₂
This theorem states that in a 2-dimensional oriented vector space over the real numbers with the properties of a normed additive commutative group, inner product space, and metric space, if the sign of the oriented angle between three points is positive (which corresponds to a counterclockwise orientation), then the first two points of these three points cannot be the same.
More concisely: In a 2-dimensional real vector space with norm, additive and commutative group structure, inner product, and metric properties, three distinct points with a positive oriented angle between any pair form a triangle.
|
EuclideanGeometry.right_ne_of_oangle_ne_zero
theorem EuclideanGeometry.right_ne_of_oangle_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₃ ≠ p₂
This theorem, from the field of Euclidean Geometry, states that if the angle formed by three points, `p₁`, `p₂`, and `p₃`, is not zero, then the last two points, `p₂` and `p₃`, cannot be the same point. The theorem is formulated in the context of vector spaces and requires that the underlying space `V` be a 2-dimensional, real inner product space. It also requires that `V` is given an orientation.
More concisely: In a 2-dimensional, real inner product space with orientation, distinct points `p₁`, `p₂`, and `p₃` form a non-collinear triangle if and only if the angle between the vectors `p₁-p₂` and `p₂-p₃` is non-zero.
|
EuclideanGeometry.oangle_eq_oangle_of_dist_eq
theorem EuclideanGeometry.oangle_eq_oangle_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
dist p₁ p₂ = dist p₁ p₃ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₂ p₃ p₁
This theorem is an oriented angle-at-point form of the Pons Asinorum, also known as the Isosceles Triangle Theorem. It states that for a given vector space `V`, point space `P`, inner product space over real numbers, metric space, normed add torsor, given the fact that the finite rank of the vector space `V` over real numbers is 2 and it is oriented, then for any three points `p₁`, `p₂`, and `p₃`, if the distance between `p₁` and `p₂` is equal to the distance between `p₁` and `p₃`, then the oriented angle `oangle` of `p₁`, `p₂`, and `p₃` is equal to the oriented angle `oangle` of `p₂`, `p₃`, and `p₁`. This theorem aims to express the basic geometrical concept that in an isosceles triangle, the base angles are equal.
More concisely: In an oriented 2-dimensional vector space over the real numbers, if the distances between any two points form an isosceles triangle, then the oriented angles opposite the equal sides are equal.
|
EuclideanGeometry.right_ne_of_oangle_eq_neg_pi_div_two
theorem EuclideanGeometry.right_ne_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → p₃ ≠ p₂
This theorem states that in a two-dimensional Euclidean space, if the oriented angle between three points `p₁`, `p₂`, and `p₃` is negative half of π (which is `-π/2`), then the last two points `p₂` and `p₃` cannot be the same. Here, the oriented angle is defined in terms of the inner product and norm on the underlying vector space, and the space is assumed to be oriented.
More concisely: In a two-dimensional Euclidean space with an oriented inner product, if the oriented angle between vectors `p₁ - p₃` and `p₂ - p₃` is `-π/2`, then `p₂ ≠ p₃`.
|
EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq
theorem EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
dist p₁ p₂ = dist p₁ p₃ → |(EuclideanGeometry.oangle p₁ p₂ p₃).toReal| < Real.pi / 2
This theorem states that for any isosceles triangle in a 2-dimensional inner product space (a space where distances and angles can be measured), the magnitude of the base angle, when expressed in radians, is less than π/2. Here, the isosceles triangle is understood as a triangle with one distinguished point `p₁` and two other points `p₂` and `p₃` such that the distance from `p₁` to `p₂` is equal to the distance from `p₁` to `p₃`. The base angle is the angle at the distinguished point `p₁` between the lines connecting `p₁` to `p₂` and `p₁` to `p₃`. The theorem applies to real vector spaces that are oriented, meaning that a consistent choice of rotation direction (clockwise or counterclockwise) has been made. The result is universal, as it doesn't depend on any specifics about the triangle except that it is isosceles.
More concisely: In an oriented 2-dimensional real inner product space, the base angle of an isosceles triangle is less than π/2 radians.
|
EuclideanGeometry.oangle_midpoint_rev_left
theorem EuclideanGeometry.oangle_midpoint_rev_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle (midpoint ℝ p₂ p₁) p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃
The theorem `EuclideanGeometry.oangle_midpoint_rev_left` states that in a 2-dimensional real inner product space, the oriented angle formed by three points is unchanged even if the first point is replaced by the midpoint of the segment between the first and the second point. In other words, if we have three points `p₁`, `p₂`, and `p₃`, the oriented angle formed by `p₁`, `p₂`, and `p₃` is the same as the oriented angle formed by the midpoint of `p₁` and `p₂`, `p₂`, and `p₃`. This theorem is applicable under the conditions that the vector space `V` is a normed add commutative group, there is an inner product defined over `V` with `ℝ` as the field of scalars, `P` is a metric space, `V` is a normed add torsor over `P`, and that `V` is an oriented 2-dimensional module over `ℝ`.
More concisely: In an oriented 2-dimensional real inner product space, the oriented angle between the first point, the second point, and the third point is equal to the oriented angle between the midpoint of the segment between the first and second points, the second point, and the third point.
|
EuclideanGeometry.left_ne_of_oangle_sign_ne_zero
theorem EuclideanGeometry.left_ne_of_oangle_sign_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₁ ≠ p₂
This theorem, from the field of Euclidean Geometry, states that: given a normed additive commutative group `V`, an inner product space over the reals `ℝ` on `V`, a metric space `P`, a normed additive torsor connecting `V` and `P`, and a 2-dimensional real vector space `ℝ V` with an orientation, if the sign of the oriented angle between three points `p₁`, `p₂`, and `p₃` is not zero, then the first two points `p₁` and `p₂` must be distinct. In other words, if there's a non-zero signed angle between three points, the first two of those points cannot be the same.
More concisely: If three points in a normed additive commutative group with an inner product, a metric space, and an oriented 2-dimensional real vector space have a non-zero signed angle between them, then they are distinct.
|
EuclideanGeometry.oangle_rev
theorem EuclideanGeometry.oangle_rev :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
EuclideanGeometry.oangle p₃ p₂ p₁ = -EuclideanGeometry.oangle p₁ p₂ p₃
The theorem `EuclideanGeometry.oangle_rev` states that for any three points `p₁`, `p₂`, and `p₃` in a 2-dimensional Euclidean space over the reals with a given orientation, the oriented angle `oangle` from `p₃` to `p₂` then to `p₁` is the negative of the oriented angle from `p₁` to `p₂` then to `p₃`. Here, `oangle` is a function representing the oriented angle between three points. This implies that reversing the order of the points results in an orientation-reversed angle.
More concisely: The oriented angle from point `p₃` to `p₂` then to `p₁` is the negative of the oriented angle from `p₁` to `p₂` then to `p₃` in a 2-dimensional Euclidean space.
|
Collinear.oangle_sign_of_sameRay_vsub
theorem Collinear.oangle_sign_of_sameRay_vsub :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (p₅ : P),
p₁ ≠ p₂ →
p₃ ≠ p₄ →
Collinear ℝ {p₁, p₂, p₃, p₄} →
SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃) →
(EuclideanGeometry.oangle p₁ p₅ p₂).sign = (EuclideanGeometry.oangle p₃ p₅ p₄).sign
The theorem states that given a line with four distinct points, and a fifth point off the line, if the vectors connecting the first and second point, and the third and fourth point, are aligned in the same direction along the line, then the angles formed by the line segments connecting the fifth point to the first and second points, and the fifth point to the third and fourth points, will have the same sign. This is under the conditions that the vector space has a finite rank of 2 and an orientation, and that the underlying field of the vector space is the real numbers.
More concisely: Given a line in a 2-dimensional real vector space with orientation and a fifth point off the line such that the vectors formed by the line segments between adjacent points are collinear, then the signed angles between the fifth point and the first and second points, and between the fifth point and the third and fourth points, have the same sign.
|
EuclideanGeometry.oangle_self_right
theorem EuclideanGeometry.oangle_self_right :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ : P), EuclideanGeometry.oangle p₁ p₂ p₂ = 0
This theorem, named "EuclideanGeometry.oangle_self_right", is about the angle created by three points in a space. Specifically, it states that the angle ∡ABB at a point is always zero. The theorem takes as parameters: two types `V` and `P`, where `V` is a normed add commutative group and also an inner product of real numbers, while `P` is a metric space as well as a normed add torsor over `V`. Additionally, the rank of `V` over the field of real numbers (ℝ) is assumed to be 2, and `V` is assumed to be an oriented module over ℝ. The theorem then asserts that for any two points `p₁` and `p₂`, the angle at `p₂` (\(∡p₁p₂p₂\)) is always 0.
More concisely: In a 2-dimensional oriented inner product space `V` over the real numbers, with `P` as a metric space and normed add torsor over `V`, the angle between any two vectors `p₁` and `p₂` based at point `p₂` is zero.
|
EuclideanGeometry.left_ne_right_of_oangle_eq_pi
theorem EuclideanGeometry.left_ne_right_of_oangle_eq_pi :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi → p₁ ≠ p₃
This theorem belongs to the domain of Euclidean Geometry, and it states that given a 2-dimensional real inner product space, if the angle between three distinct points, denoted as `p₁`, `p₂`, and `p₃`, is equal to `π` radians (which is equivalent to a straight line or 180 degrees), then the first and third points, `p₁` and `p₃`, cannot be the same.
More concisely: In a 2-dimensional real inner product space, if the angle between three distinct points is π radians (180 degrees), then the first and third points are not equal.
|
EuclideanGeometry.oangle_rotate_sign
theorem EuclideanGeometry.oangle_rotate_sign :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
(EuclideanGeometry.oangle p₂ p₃ p₁).sign = (EuclideanGeometry.oangle p₁ p₂ p₃).sign
This theorem states that rotating the points in an oriented angle doesn't alter the sign of that angle. More precisely, given a vector space `V` over the real numbers `ℝ` that is a normed add commutative group, an inner product space, and a metric space `P` that is a normed additive group with a translation action by `V`, and assuming `V` is two-dimensional and oriented, for any three points `p₁`, `p₂`, and `p₃` in `P`, the sign of the oriented angle from `p₂` to `p₃` around `p₁` will be the same as the sign of the oriented angle from `p₁` to `p₂` around `p₃`. The sign of an angle is defined as `0` if the angle is `0` or `π`, `1` if the angle is strictly between `0` and `π`, and `-1` if the angle is strictly between `-π` and `0`. This sign is determined by the sign of the sine of the angle.
More concisely: Given two-dimensional oriented vector spaces over the real numbers with the given properties, the sign of the angle between any two vectors remains constant under rotation around a third vector.
|
EuclideanGeometry.left_ne_right_of_oangle_sign_ne_zero
theorem EuclideanGeometry.left_ne_right_of_oangle_sign_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign ≠ 0 → p₁ ≠ p₃
This theorem states that in a two-dimensional oriented inner product space (real vector space equipped with an inner product and an orientation), if there are three points such that the signed angle between them is not zero, then the first and third points must be distinct. This theorem is a part of Euclidean geometry, which is the study of plane geometry based on certain axioms.
More concisely: In a two-dimensional oriented inner product space, if the signed angle between three distinct points is non-zero, then the first and third points are distinct.
|
EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint
theorem EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p : P},
p₁ ≠ p₂ →
(dist p₁ p = dist p₂ p ↔
∃ r, r • (EuclideanGeometry.o.rotation ↑(Real.pi / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p)
This theorem, `EuclideanGeometry.dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint`, states that in a two-dimensional Euclidean space, if we have three points `p₁`, `p₂`, and `p`, where `p₁` and `p₂` are distinct, then `p₁` and `p₂` are equidistant from `p` if and only if `p` can be represented as the sum of the midpoint of `p₁` and `p₂` and a vector that is a multiple of a 90 degree (or `π / 2` radians) rotation of the vector from `p₁` to `p₂`. The multiple is denoted as `r` in the theorem.
More concisely: In a two-dimensional Euclidean space, points `p₁` and `p₂` are equidistant from point `p` if and only if `p` is the midpoint of `p₁` and `p₂` plus or minus a multiple of the 90-degree rotation of the vector from `p₁` to `p₂`.
|
Wbtw.oangle_eq_left
theorem Wbtw.oangle_eq_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₁' p₂ p₃ : P},
Wbtw ℝ p₂ p₁ p₁' → p₁ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁' p₂ p₃
This theorem states that the oriented angle between three points in a 2-dimensional Euclidean space remains unchanged if the first point is replaced by another point that lies weakly between the original first point and the second one. An "oriented angle" here refers to an angle measurement that retains a sense of rotation (clockwise or counterclockwise). The term "weakly between" is used to indicate that the new point can coincide with one of the original points. The precondition of the theorem ensures that the first and the second points are distinct.
More concisely: The theorem asserts that the oriented angle between two points in a 2-D Euclidean space remains unchanged when replaced by another point lying on the segment connecting them.
|
EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear
theorem EuclideanGeometry.oangle_eq_zero_or_eq_pi_iff_collinear :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ Collinear ℝ {p₁, p₂, p₃}
This theorem states that given a set of three points `p₁`, `p₂`, and `p₃` in a Euclidean Geometry with a two-dimensional real-valued vector space, the oriented angle formed by these points is either `0` or `π` (pi) if and only if these points are collinear. Here, collinearity of points implies that the points all lie on a single straight line. The oriented angle is a geometric quantity that measures the angle in a specific orientation (clockwise or counterclockwise). The vector space is assumed to be equipped with an inner product (a generalization of the dot product) and a metric space structure (which allows for the concept of distance between points).
More concisely: In Euclidean Geometry with a two-dimensional real-valued vector space equipped with an inner product and metric space structure, the oriented angle between three collinear points `p₁`, `p₂`, and `p₃` is either 0 or π.
|
EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.right_ne_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₃ ≠ p₂
This theorem, from Euclidean Geometry, states that if the angle formed by three points is equal to `π / 2` (or 90 degrees), then the last two points are not the same. This is true in a two-dimensional vector space over the field of real numbers. The angle is calculated using the inner product space structure of the vector space, and the points are considered in a metric space structure.
More concisely: In a 2-dimensional real vector space with inner product structure, if the angle between any two distinct vectors is 90 degrees, then the vectors are orthogonal and not equal.
|
Wbtw.oangle₁₃₂_eq_zero
theorem Wbtw.oangle₁₃₂_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Wbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₁ p₃ p₂ = 0
This theorem states that if in a two-dimensional oriented inner product space, the second of three points is weakly between the other two points, then the oriented angle at the third point (when taken in the opposite order or reversed) is zero. The weak betweenness is defined in terms of an affine segment. Here, the points and the vectors between them live in a normed add-torsor and a normed add-commutative group respectively. The oriented angle is computed on a Euclidean Geometry setup.
More concisely: In a two-dimensional oriented inner product space, if point B is weakly between A and C (in the affine sense), then the oriented angle at C between the vectors AB and BC is zero.
|
EuclideanGeometry.left_ne_right_of_oangle_eq_pi_div_two
theorem EuclideanGeometry.left_ne_right_of_oangle_eq_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → p₁ ≠ p₃
This theorem from the Euclidean Geometry in Lean 4 states that, for a real inner product space `V` of dimension 2, endowed with an orientation and a metric space `P` that is a normed add torsor over `V`, if the oriented angle formed by three points `p₁`, `p₂`, and `p₃` (in that order) is equal to `π / 2` (which is equivalent to a right angle in Euclidean geometry), then the first point `p₁` and the third point `p₃` are not the same point, that is, `p₁ ≠ p₃`. The oriented angle is calculated using the `EuclideanGeometry.oangle` function which gives the angle in radians (between 0 and `π`) between the three points.
More concisely: In a 2-dimensional real inner product space with orientation and metric, if the oriented angle between three distinct points is a right angle (π/2 radians), then the first and third points are not the same.
|
Sbtw.oangle₂₁₃_eq_zero
theorem Sbtw.oangle₂₁₃_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₁ p₃ = 0
This theorem states that given a normed additive commutative group `V` over a real inner product space, a metric space `P`, and an oriented module over `V` in a 2-dimensional real vector space, if a point `p₂` is strictly between two other points `p₁` and `p₃` (`p₂` is neither equal to `p₁` nor `p₃` and `p₂` is within the segment `p₁p₃`), then the oriented angle from `p₁` through `p₂` to `p₃`, denoted `EuclideanGeometry.oangle p₂ p₁ p₃`, is equal to zero. This means that in a 2-dimensional real vector space, if one point is strictly between two others, the angle at the first point targeting the middle point and then the third point is zero.
More concisely: In a 2-dimensional real vector space, the oriented angle from a point strictly between two other points to the middle point and then to the third point equals zero.
|
EuclideanGeometry.oangle_eq_zero_iff_wbtw
theorem EuclideanGeometry.oangle_eq_zero_iff_wbtw :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ p₂ p₃ p₁
This theorem, from the field of Euclidean Geometry, states that the oriented angle between three points (p₁, p₂, p₃) is zero if and only if one of the first (p₁) and third (p₃) points is weakly between the other two. The "weakly between" condition is defined in the context of an ordered ring and an affine torsor, and it means that one point lies within the affine segment formed by the other two. This theorem applies in a 2-dimensional vector space over the real numbers. It is important to note that the vector space is normed and has an inner product, and points in the space are measured using a metric space structure.
More concisely: In a 2-dimensional Euclidean vector space with an inner product, the oriented angle between three points is zero if and only if one point is collinear and lies between the other two.
|
EuclideanGeometry.right_ne_of_oangle_sign_eq_one
theorem EuclideanGeometry.right_ne_of_oangle_sign_eq_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₃ ≠ p₂
The theorem `EuclideanGeometry.right_ne_of_oangle_sign_eq_one` states that in a Euclidean space, if the sign of the angle between three points is positive, then the last two points are distinct. The theorem is applicable in a 2-dimensional vector space over the real numbers, equipped with the standard inner product, metric space, and orientation. Specifically, if you have three points `p₁`, `p₂`, and `p₃` such that the oriented angle from `p₁` to `p₂` to `p₃` is positive (sign equals 1), then `p₃` and `p₂` are not the same point.
More concisely: In a Euclidean 2-dimensional space over the real numbers, if the signed angle between three points is positive, then the last two points are distinct.
|
Sbtw.oangle₂₃₁_eq_zero
theorem Sbtw.oangle₂₃₁_eq_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.oangle p₂ p₃ p₁ = 0
The theorem `Sbtw.oangle₂₃₁_eq_zero` states that for any three points `p₁`, `p₂`, and `p₃` in a normed add-torsor over a normed add commutative group which is an inner product space over the `Real` numbers, if the space is 2-dimensional and has defined orientation and if the point `p₂` is strictly between `p₁` and `p₃` (according to the definition of `Sbtw`), then the oriented angle at `p₃`, defined as `EuclideanGeometry.oangle p₂ p₃ p₁`, is equal to zero. This essentially means that in a 2-dimensional oriented vector space, if a point is strictly between two others, the angle at the third point (defined in terms of the second and first points) is zero.
More concisely: In a 2-dimensional inner product space over the Real numbers with defined orientation, if point `p₂` is strictly between points `p₁` and `p₃`, then the oriented angle from `p₁` to `p₃` via `p₂` is equal to zero.
|
EuclideanGeometry.left_ne_of_oangle_sign_eq_neg_one
theorem EuclideanGeometry.left_ne_of_oangle_sign_eq_neg_one :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₁ ≠ p₂
This theorem from Euclidean Geometry states that given a 2-dimensional vector space `V` over real numbers, with `P` as the associated normed add-torsor, if the oriented angle of three points `p₁`, `p₂`, `p₃` in `P` is negative (specifically -1), then the first two points `p₁` and `p₂` are distinct, i.e., they are not equal. This establishes a connection between the orientation of the angle and the non-equality of the defining points.
More concisely: In Euclidean geometry, if the oriented angle between two vectors in a 2-dimensional real vector space is -1 radians, then those vectors are distinct.
|
Sbtw.oangle_sign_eq_left
theorem Sbtw.oangle_sign_eq_left :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (p₄ : P),
Sbtw ℝ p₁ p₂ p₃ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = (EuclideanGeometry.oangle p₁ p₄ p₃).sign
The theorem `Sbtw.oangle_sign_eq_left` states that given three points `p₁`, `p₂`, and `p₃` in strict order on the same line and a fourth point `p₄`, the angles at `p₄` between `p₁` and `p₂` or `p₁` and `p₃` have the same sign. This is under the context that the vector space `V` is a normed add commutative group as well as an inner product space over the real numbers, `ℝ`, and `P` is a metric space with a normed add-torsor structure over `V`. The dimension of `V` over `ℝ` is assumed to be 2, and `V` is also equipped with an oriented module structure over `ℝ`. The strict ordering of the three points is defined by the `Sbtw` definition, meaning `p₂` is strictly between `p₁` and `p₃`, and `p₂` is not equal to `p₁` or `p₃`. The sign of an angle is defined by the function `EuclideanGeometry.oangle` and its `sign` method.
More concisely: Given three collinear points `p₁`, `p₂`, and `p₃` in strict order, and a fourth point `p₄`, the angles at `p₄` between `p₁` and `p₂` and between `p₁` and `p₃` have the same sign.
|
EuclideanGeometry.oangle_swap₁₂_sign
theorem EuclideanGeometry.oangle_swap₁₂_sign :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] (p₁ p₂ p₃ : P),
-(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₂ p₁ p₃).sign
This theorem states that if you swap the first and second points in an oriented angle, it negates the sign of that angle. More specifically, given a normed additive commutative group `V`, an inner product space over the real numbers on `V`, a metric space on `P`, and a normed additive torsor `V` on `P`, if the finite rank of `V` over the reals is 2 and the orientation of `V` is given by `Fin 2`, then for any three points `p₁`, `p₂`, and `p₃` in `P`, the negative sign of the oriented angle formed by `p₁`, `p₂`, and `p₃` is equal to the sign of the oriented angle formed by `p₂`, `p₁`, and `p₃`. This essentially captures the geometric intuition that swapping the two points defining an angle effectively reflects that angle in a mirror, thus flipping its sign.
More concisely: Given a 2-dimensional real inner product space `V` with orientation `Fin 2`, the signed angle between two points in the associated metric space is negated when the order of the points is reversed.
|
EuclideanGeometry.left_ne_right_of_oangle_ne_zero
theorem EuclideanGeometry.left_ne_right_of_oangle_ne_zero :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ ≠ 0 → p₁ ≠ p₃
This theorem states that in a two-dimensional oriented module over real numbers, if the angle formed by three points is non-zero, then the first and third points cannot be identical. The points belong to a space that is a normed additively torsor over a normed additively commutative group, and the underlying vector space is an inner product space.
More concisely: In a two-dimensional oriented real inner product space, distinct points form a non-zero angle.
|
EuclideanGeometry.oangle_add
theorem EuclideanGeometry.oangle_add :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ p₃ : P},
p₁ ≠ p →
p₂ ≠ p →
p₃ ≠ p →
EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₃
This theorem is a proposition in Euclidean Geometry, stating that given a normed additively commutative group `V`, an inner product space over `V` with real numbers, a metric space `P`, and a normed additively commutative torsor `P` over `V`, with the finite rank of `V` being 2 and given an orientation on the 2-dimensional `V`, if we have four points `p`, `p₁`, `p₂`, `p₃` such that `p₁`, `p₂`, `p₃` are not equal to `p`, then the sum of the angle between `p₁` and `p₂` at `p` and the angle between `p₂` and `p₃` at `p` is equal to the angle between `p₁` and `p₃` at `p`. This is a fundamental theorem in geometry, often referred to as the Angle Addition Postulate.
More concisely: In Euclidean geometry, given a 2-dimensional oriented inner product space `V` with real numbers, the sum of the angles between any three non-coinciding points `p₁, p₂, p₃` at a fixed point `p` is equal to the angle between `p₁` and `p₃`.
|
AffineSubspace.SOppSide.oangle_sign_eq_neg
theorem AffineSubspace.SOppSide.oangle_sign_eq_neg :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {s : AffineSubspace ℝ P} {p₁ p₂ p₃ p₄ : P},
p₁ ∈ s →
p₂ ∈ s →
s.SOppSide p₃ p₄ → (EuclideanGeometry.oangle p₁ p₄ p₂).sign = -(EuclideanGeometry.oangle p₁ p₃ p₂).sign
This theorem states that in a real 2-dimensional vector space with an associated affine subspace, given two points (`p₁`, `p₂`) within this affine subspace, and two other points (`p₃`, `p₄`) on opposite sides of this subspace, the sign of the angle (`oangle`) between `p₁` and `p₂` at `p₄` is the negative of the sign of the angle between `p₁` and `p₂` at `p₃`. This theorem holds under the conditions that the vector space is a normed additive commutative group, it is equipped with an inner product and a metric, and it is oriented.
More concisely: In a real 2-dimensional oriented normed additive commutative group with an inner product and metric, the sign of the angle between two vectors at a point on each side of an affine subspace is opposite.
|
EuclideanGeometry.oangle_add_swap
theorem EuclideanGeometry.oangle_add_swap :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ p₃ : P},
p₁ ≠ p →
p₂ ≠ p →
p₃ ≠ p →
EuclideanGeometry.oangle p₂ p p₃ + EuclideanGeometry.oangle p₁ p p₂ = EuclideanGeometry.oangle p₁ p p₃
This theorem is a statement in Euclidean geometry about the angles formed by three points with respect to a reference point `p`. Specifically, it states that given a two-dimensional vector space `V` over the real numbers, a metric space `P`, and a normed add torsor `V P`, if the points `p₁`, `p₂`, and `p₃` are not equal to `p`, then the sum of the angle `(p₂, p, p₃)` and the angle `(p₁, p, p₂)` equals the angle `(p₁, p, p₃)`. This is analogous to the familiar geometric concept that the sum of the angles at a point is constant.
More concisely: In a 2-dimensional vector space over the real numbers with a metric space and a normed additive torsor, the sum of the angles between any three distinct points and a reference point is constant.
|
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two
theorem EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] [hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)]
[inst_4 : Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P},
EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2) → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
The theorem states that if the oriented angle between three points, `p₁`, `p₂`, and `p₃`, in a two-dimensional Euclidean space is `-π / 2`, then the unoriented angle between these three points is `π / 2`. Here, an oriented angle refers to an angle that takes into account the direction of rotation (counter-clockwise or clockwise), while an unoriented angle only considers the magnitude of the angle without considering the direction of rotation. It's worth noting that the space is assumed to be a 2-dimensional vector space over real numbers in this context.
More concisely: If the oriented angle between three points in a 2-dimensional Euclidean space is `-π/2`, then the unoriented angle is `π/2`.
|