EuclideanGeometry.angle_nonneg
theorem EuclideanGeometry.angle_nonneg :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (p1 p2 p3 : P), 0 ≤ EuclideanGeometry.angle p1 p2 p3
The theorem `EuclideanGeometry.angle_nonneg` states that the angle at a point in a Euclidean space is always nonnegative. More specifically, for any three points `p1`, `p2`, and `p3` in a space endowed with a normed additively commutative group structure, inner product space over the real numbers, metric space, and normed additive torsor, the angle at `p2` between the line segments towards `p1` and `p3` (denoted as `EuclideanGeometry.angle p1 p2 p3`) is always greater than or equal to zero.
More concisely: The angle between any two line segments in a Euclidean space with respect to a common endpoint is a non-negative measure.
|
EuclideanGeometry.sin_pos_of_not_collinear
theorem EuclideanGeometry.sin_pos_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → 0 < (EuclideanGeometry.angle p₁ p₂ p₃).sin
This theorem states that given three points `p₁`, `p₂`, and `p₃` in a metric space with an associated normed add torsor, and an inner product space over the real numbers, if these three points are not collinear (meaning the set of these points doesn't form a straight line), then the sine of the angle at `p₂` between the line segments towards `p₁` and `p₃` is positive. Essentially, this tells us that if three points don't line up in a straight line, they form an open angle with a positive sine value.
More concisely: In a metric space with an associated normed add torsor and an inner product space over the real numbers, the sine of the angle between the line segments from points `p₁`, `p₂`, and `p₃` is positive if and only if `p₁`, `p₂`, and `p₃` are not collinear.
|
AffineIsometry.angle_map
theorem AffineIsometry.angle_map :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4}
[inst_4 : NormedAddCommGroup V₂] [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂]
[inst_7 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ] P₂) (p₁ p₂ p₃ : P),
EuclideanGeometry.angle (f p₁) (f p₂) (f p₃) = EuclideanGeometry.angle p₁ p₂ p₃
The theorem `AffineIsometry.angle_map` states that for any real affine isometry `f` and any three points `p1`, `p2`, `p3` in a given metric space with inner product and normed add torsor, the angle at the image of `p2` under `f`, between the line segments to the images of `p1` and `p3` is equal to the angle at `p2` between the line segments to `p1` and `p3`. Thus, this theorem shows that affine isometries preserve the angle between line segments.
More concisely: The theorem `AffineIsometry.angle_map` asserts that given any real affine isometry `f` and points `p1`, `p2`, `p3` in a metric space with inner product and normed add torsor, the angle between the line segments from `p1` to `p2` and from `p1` to `p3` is equal to the angle between the line segments from `f(p2)` to `f(p1)` and from `f(p2)` to `f(p3)`.
|
EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero
theorem EuclideanGeometry.dist_eq_abs_sub_dist_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] {p1 p2 p3 : P},
p1 ≠ p2 → p3 ≠ p2 → (dist p1 p3 = |dist p1 p2 - dist p3 p2| ↔ EuclideanGeometry.angle p1 p2 p3 = 0)
The theorem `EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero` states that for a given three points A, B, and C in a Euclidean space, where A is not equal to B and C is not equal to B, the angle ∠ABC is equal to 0 (meaning A, B, and C are collinear) if and only if the distance between A and C is equal to the absolute difference between the distance from A to B and the distance from B to C.
More concisely: In a Euclidean space, points A, B, and C are collinear if and only if the distance from A to C equals the absolute difference between the distances from A to B and B to C.
|
EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw
theorem EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ = p₃ ∧ p₁ ≠ p₂ ∨ Sbtw ℝ p₂ p₁ p₃ ∨ Sbtw ℝ p₂ p₃ p₁
The theorem `EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw` states that for any given three points `p₁`, `p₂` and `p₃` in a Euclidean Geometry, the angle formed at `p₂` by the line segments to `p₁` and `p₃` is zero if and only if either `p₁` and `p₃` are the same point and are different from `p₂`, or `p₁` or `p₃` is strictly between `p₂` and the other point. Here, "strictly between" means that `p₁` or `p₃` lies between the other two points and is not equal to either of them.
More concisely: In Euclidean Geometry, the angle between line segments from points `p₁` and `p₂`, and from `p₁` and `p₃`, is zero if and only if `p₁` is the same point as `p₃` or `p₁` is strictly between `p₂` and `p₃`, or vice versa.
|
EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi
theorem EuclideanGeometry.right_dist_ne_zero_of_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = Real.pi → dist p3 p2 ≠ 0
This theorem in the Euclidean Geometry context states that: If the undirected angle at point B (p2) between the line segments to points A (p1) and C (p3) equals π (or 180°), then the distance from C (p3) to B (p2) is not zero. This essentially means that if the angle is flat (180 degrees), then the two points forming the angle are not the same point, and hence they have a non-zero distance.
More concisely: In Euclidean geometry, if the angle between line segments from points A and C to point B is a flat angle of 180 degrees, then the distance from C to B is positive.
|
EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw
theorem EuclideanGeometry.angle_eq_zero_iff_ne_and_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = 0 ↔ p₁ ≠ p₂ ∧ Wbtw ℝ p₂ p₁ p₃ ∨ p₃ ≠ p₂ ∧ Wbtw ℝ p₂ p₃ p₁
The theorem `EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw` states that for any three points `p₁`, `p₂`, and `p₃` in a Euclidean space, the angle at `p₂` between the line segments to `p₁` and `p₃` is zero if and only if one of the following two conditions is satisfied:
- `p₁` is not equal to `p₂` and `p₁` is weakly between `p₂` and `p₃`, or
- `p₃` is not equal to `p₂` and `p₃` is weakly between `p₂` and `p₁`.
Here, a point `y` is said to be weakly between `x` and `z` if `y` is in the affine segment between `x` and `z`.
More concisely: The angle between the line segments from a point to two other distinct points in a Euclidean space is zero if and only if one of the points is weakly between the other two.
|
EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi
theorem EuclideanGeometry.angle_add_angle_eq_pi_of_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] (p1 : P) {p2 p3 p4 : P},
EuclideanGeometry.angle p2 p3 p4 = Real.pi →
EuclideanGeometry.angle p1 p3 p2 + EuclideanGeometry.angle p1 p3 p4 = Real.pi
This theorem states that in the context of a normed add torsor over an inner product space, if the undirected angle at point B (referred to as `p3` in the theorem) between the line segments to C (`p4`) and D (`p2`) is equal to pi (π), then the sum of the undirected angles at point B between line segments to A (`p1`) and C, and between line segments to A and D, is also equal to pi. In other words, if the angle ∠BCD is π, then the sum of the angles ∠ACB and ∠ACD is also π. This is a property of Euclidean geometry.
More concisely: In a normed add torsor over an inner product space, if the angle between line segments from point B to C and from point B to D is π, then the sum of the angles between line segments from A to B and from A to C, and between line segments from A to B and from A to D, is also π.
|
Sbtw.angle₁₂₃_eq_pi
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
The theorem `Sbtw.angle₁₂₃_eq_pi` states that given normed additive commutative group `V`, inner product space `V` over real numbers, metric space `P`, and normed additive torsor `V` over `P`, for any three points `p₁`, `p₂`, and `p₃` in `P`, if point `p₂` is strictly between points `p₁` and `p₃`, then the undirected angle at `p₂` between the line segments `p₁p₂` and `p₂p₃` is equal to π (pi). This theorem essentially says in a Euclidean geometry context that if a point lies strictly between two other points, the angle it forms with them is a straight angle (180 degrees, or π in radians).
More concisely: Given a normed additive commutative group `V` with an inner product, metric space `P`, and a normed additive torsor `V` over `P`, the undirected angle between line segments `p₁p₂` and `p₂p₃` is equal to π (pi radians) when `p₂` is strictly between `p₁` and `p₃`.
|
Wbtw.angle₂₃₁_eq_zero_of_ne
theorem Wbtw.angle₂₃₁_eq_zero_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → EuclideanGeometry.angle p₂ p₃ p₁ = 0
This theorem states that given three points, if the second point is weakly between the first and the third, and the second and third points are not identical, then the angle at the third point (formed by the line segments from the third point to the second point and from the third point to the first point) is zero. In other words, if we have three points, with the second point either on the line segment between the first and third or beyond the first point, and the second point is distinct from the third, the direction from the third point towards the second point is the same as the direction from the third point towards the first point.
More concisely: If points $A$, $B$, and $C$ are distinct with $B$ on the segment $AC$ or beyond it, then the angle at $C$ formed by the lines $AC$ and $BC$ is zero.
|
EuclideanGeometry.angle_eq_pi_iff_sbtw
theorem EuclideanGeometry.angle_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi ↔ Sbtw ℝ p₁ p₂ p₃
The theorem states that for any three points `p₁`, `p₂`, and `p₃` in a metric space, the angle at `p₂` between line segments to `p₁` and `p₃` is equal to π (in radians) if and only if `p₂` is strictly between `p₁` and `p₃`. Here, being "strictly between" means that `p₂` lies on the line segment from `p₁` to `p₃`, but is not identical to `p₁` or `p₃`. This theorem connects the geometric concept of being "between" two other points with the trigonometric concept of an angle measuring π radians (or 180 degrees).
More concisely: In a metric space, the angle at a strictly between point between two other points is equal to π radians.
|
EuclideanGeometry.collinear_of_angle_eq_pi
theorem EuclideanGeometry.collinear_of_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → Collinear ℝ {p₁, p₂, p₃}
The theorem `EuclideanGeometry.collinear_of_angle_eq_pi` states that for any three points `p₁`, `p₂`, and `p₃` in a Euclidean space (a space equipped with the structure of a normed add torsor over an inner product space of real numbers), if the angle at `p₂` between the line segments to `p₁` and `p₃` is equal to π (pi), then these three points are collinear. In other words, given the necessary structure on the space, if the angle between line segments `p₁p₂` and `p₂p₃` is 180 degrees (π radians), then the points `p₁`, `p₂`, and `p₃` all lie on the same straight line.
More concisely: If the angle between line segments connecting three points in a Euclidean space is 180 degrees (π radians), then these points are collinear.
|
EuclideanGeometry.sin_ne_zero_of_not_collinear
theorem EuclideanGeometry.sin_ne_zero_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → (EuclideanGeometry.angle p₁ p₂ p₃).sin ≠ 0
The theorem states that if three points are not collinear, meaning they don't all fall on the same line, then the sine of the angle between these points is not zero. This is true in a Euclidean space with an inner product operation, a metric space property, and a normed add torsor structure. The collinearity of points is assessed by the `Collinear` function, which defines a set of points as being collinear if their vector span has at most dimension one. The `EuclideanGeometry.angle` function is used to measure the undirected angle at the second point between the line segments extending to the first and third points.
More concisely: In a Euclidean space equipped with an inner product operation, if three points are not collinear, then the angle between them is non-zero.
|
Sbtw.angle₃₁₂_eq_zero
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₃ p₁ p₂ = 0
This theorem states that, given a normed additive commutative group `V`, a metric space `P` that is also a normed add torsor over `V`, and three points `p₁`, `p₂`, and `p₃` in `P`, if `p₂` is strictly between `p₁` and `p₃` (defined by the `Sbtw` relation), then the undirected angle at `p₁` between the line segments to `p₂` and `p₃` (which is reversed, hence referring to `p₃ p₁ p₂` instead of `p₁ p₂ p₃`), is zero. The undirected angle is calculated using the inner product of the vectors formed by subtracting the coordinates of `p₂` and `p₃` from `p₁`.
More concisely: Given a normed additive commutative group `V`, a normed additive torsor `P` over `V`, and points `p₁`, `p₂`, `p₃` in `P` with `p₂` strictly between `p₁` and `p₃`, the undirected angle at `p₁` between the line segments `[p₁, p₂]` and `[p₂, p₃]` is zero, where the angle is calculated as the inner product of the vectors formed by the differences of their coordinates.
|
EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero
theorem EuclideanGeometry.dist_eq_abs_sub_dist_of_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = 0 → dist p1 p3 = |dist p1 p2 - dist p3 p2|
This theorem states that in a Euclidean Geometry, if the angle formed between points A (p1), B (p2), and C (p3) is zero, then the distance between points A and C is equal to the absolute value of the difference between the distance from A to B and the distance from B to C. This can be represented mathematically as: if ∠ABC = 0, then |AC| = |AB - BC|. It's important to note that the distance and angle measurements are made in a space equipped with an inner product space structure and a metric space structure.
More concisely: In Euclidean geometry, if angle ABC is zero, then the distance between points A and C equals the absolute difference of the distances from A to B and B to C: |AC| = |AB - BC|.
|
EuclideanGeometry.cos_eq_one_iff_angle_eq_zero
theorem EuclideanGeometry.cos_eq_one_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).cos = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0
The theorem states that for any three points `p₁ p₂ p₃` in a metric space with associated normed add torsor and inner product space, the cosine of the angle at `p₂` between line segments to `p₁` and `p₃` is equal to 1 if and only if the angle itself is equal to 0. This is consistent with the trigonometric fact that the cosine of 0 degrees (or 0 radians) is 1.
More concisely: In a metric space with an associated normed add torsor and inner product space, the cosine of the angle between line segments from a point to another two points is equal to 1 if and only if the angle itself is 0.
|
EuclideanGeometry.angle_const_add
theorem EuclideanGeometry.angle_const_add :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V),
EuclideanGeometry.angle (v + v₁) (v + v₂) (v + v₃) = EuclideanGeometry.angle v₁ v₂ v₃
The theorem `EuclideanGeometry.angle_const_add` states that angles in a vector space are translation invariant. This means that for any vector space `V` which is a normed add commutative group, and an inner product space over real numbers, and for any vectors `v`, `v₁`, `v₂`, and `v₃` in `V`, the angle at `v + v₂` between the line segments to `v + v₁` and `v + v₃` is identical to the angle at `v₂` between the line segments to `v₁` and `v₃`. This signifies that shifting the vectors by `v` does not alter the angle between them.
More concisely: The angle between two vectors in a normed add commutative group and inner product space over the real numbers is translation invariant.
|
EuclideanGeometry.angle_eq_left
theorem EuclideanGeometry.angle_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] (p₀ p : P),
EuclideanGeometry.angle p₀ p₀ p = Real.pi / 2
This theorem states that in Euclidean Geometry, given a normed add commutative group `V`, an inner product space over `V` with real numbers, a metric space `P`, and a normed add torsor `P` over `V`, for any points `p₀` and `p` in `P`, the angle formed at `p₀` between the line segments `p₀p₀` and `p₀p` is always equal to `π/2` (half of pi, which is roughly 1.57 in decimal form). This essentially means that the angle at a point between a line segment to itself and a line segment to another point is a right angle. This theorem is an alias of `EuclideanGeometry.angle_self_left`.
More concisely: In Euclidean Geometry, for any point `p₀` and `p` in a metric space `P` over a normed add commutative group `V` with an inner product, the angle between the line segments `p₀p₀` and `p₀p` is equal to π/2.
|
EuclideanGeometry.angle_pos_of_not_collinear
theorem EuclideanGeometry.angle_pos_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → 0 < EuclideanGeometry.angle p₁ p₂ p₃
This theorem states that if three points (p₁, p₂, p₃) in an Euclidean space are not collinear, which means they do not lie on the same line, then the angle formed at p₂ by the line segments to p₁ and p₃ is positive. In other words, there is a non-zero angle between the vectors (p₁ - p₂) and (p₃ - p₂). This theorem is based on the concepts of Euclidean geometry and the inner product space over the real numbers.
More concisely: If three points in an Euclidean space are not collinear, then the angle between the vectors formed by the points and the segment connecting the first two points is positively acute.
|
EuclideanGeometry.collinear_of_sin_eq_zero
theorem EuclideanGeometry.collinear_of_sin_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).sin = 0 → Collinear ℝ {p₁, p₂, p₃}
The theorem `EuclideanGeometry.collinear_of_sin_eq_zero` states that for any three points `p₁`, `p₂`, and `p₃` in a Euclidean Geometry, if the sine of the angle at `p₂` formed by the line segments to `p₁` and `p₃` is zero, then these three points are collinear. Collinearity, here, is defined as the set of points whose vector span has dimension at most `1`. This theorem is part of the Euclidean Geometry theory in Lean 4, which deals with properties of figures and spaces based on the Euclidean axioms.
More concisely: In Euclidean Geometry, if the sine of the angle between line segments from points `p₁`, `p₂`, and `p₃` is zero, then these points are collinear.
|
Wbtw.angle₁₃₂_eq_zero_of_ne
theorem Wbtw.angle₁₃₂_eq_zero_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₃ → EuclideanGeometry.angle p₁ p₃ p₂ = 0
The theorem `Wbtw.angle₁₃₂_eq_zero_of_ne` states that for any three points `p₁`, `p₂`, and `p₃` in a metric space equipped with an inner product space over the real numbers, if point `p₂` is weakly between `p₁` and `p₃` (inclusive of `p₁` and `p₃`) and `p₂` is not equal to `p₃`, then the angle at `p₃` formed by the line segments from `p₃` to `p₁` and from `p₃` to `p₂` is zero. In other words, in this situation, `p₁`, `p₃`, and `p₂` lie on a straight line with `p₃` between `p₁` and `p₂`.
More concisely: If three points `p₁`, `p₂`, and `p₃` in a metric space with an inner product form a weakly between relation (inclusive of `p₁` and `p₃`) and `p₂` is not equal to `p₃`, then the angle between the line segments from `p₃` to `p₁` and from `p₃` to `p₂` is zero.
|
EuclideanGeometry.collinear_of_angle_eq_zero
theorem EuclideanGeometry.collinear_of_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] {p₁ p₂ p₃ : P},
EuclideanGeometry.angle p₁ p₂ p₃ = 0 → Collinear ℝ {p₁, p₂, p₃}
The theorem states that if the undirected angle at the second point between the line segments to the first and third points is zero, then the set of these three points is collinear. In other words, if the three points form an angle of zero degrees, they all lie on the same straight line. This is applicable in the context of a metric space with a normed add torsor and an inner product space over real numbers.
More concisely: In a normed additive torsor and inner product space over the real numbers, three points form a collinear configuration if and only if the angle between the line segments connecting the first and second points and the first and third points is zero.
|
EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi
theorem EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).sin = 0 ↔
EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
The theorem states that for any three points in a Euclidean space, the sine of the angle formed at the middle point by the line segments to the other two points is equal to zero if and only if the angle itself is equal to zero or π. In other words, the sine of an angle is zero when the angle is either a straight angle (π radians or 180 degrees) or a null angle (0 radians or 0 degrees).
More concisely: The sine of an angle in a Euclidean space between any three points is zero if and only if the angle is a straight angle or a null angle.
|
EuclideanGeometry.angle_neg
theorem EuclideanGeometry.angle_neg :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ : V),
EuclideanGeometry.angle (-v₁) (-v₂) (-v₃) = EuclideanGeometry.angle v₁ v₂ v₃
This theorem, named `EuclideanGeometry.angle_neg`, states that the angles in a vector space are invariant to inversion. More specifically, for any three vectors `v₁`, `v₂`, `v₃` in a vector space with a real inner product and a normed additive commutative group structure, the angle at the point `-v₂` between the line segments to `-v₁` and `-v₃` is equal to the angle at the point `v₂` between the line segments to `v₁` and `v₃`. This essentially means flipping or inverting the vectors does not change the angle between them.
More concisely: The angle between vectors `v₁` and `v₃` in a real inner product space is equal to the angle between `-v₂` and `-v₁`, and `v₂` and `v₃`.
|
EuclideanGeometry.angle_lt_pi_of_not_collinear
theorem EuclideanGeometry.angle_lt_pi_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi
This theorem states that if three points are not collinear, which means they do not lie on the same straight line, then the angle between them is less than π (or pi, which is approximately 3.14159265). This angle is measured at the second point, between the line segments that go from the second point to the first and the third point. The absence of collinearity ensures that the points form a distinct angle, which is always less than a straight angle (π radians or 180 degrees).
More concisely: If three points are non-collinear, then the angle between them is less than π radians (or 180 degrees).
|
EuclideanGeometry.angle_comm
theorem EuclideanGeometry.angle_comm :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (p1 p2 p3 : P),
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p3 p2 p1
The theorem `EuclideanGeometry.angle_comm` states that the angle at a point in a Euclidean space does not depend on the order of the other two points. That is, given any three points `p1`, `p2`, and `p3` in such a space, the angle at `p2` between the line segments to `p1` and `p3` is the same as the angle at `p2` between the line segments to `p3` and `p1`. This can be denoted mathematically as `∠ p1 p2 p3 = ∠ p3 p2 p1`. This theorem is related to the concept of symmetry in Euclidean geometry.
More concisely: The angle between two line segments in a Euclidean space, determined by their endpoints, is symmetric with respect to the order of the endpoints.
|
Sbtw.angle₁₃₂_eq_zero
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₁ p₃ p₂ = 0
The theorem `Sbtw.angle₁₃₂_eq_zero` states that for three points `p₁`, `p₂`, and `p₃` in a Euclidean space, if the second point `p₂` is strictly between the other two points `p₁` and `p₃` (meaning that `p₂` is not equal to `p₁` or `p₃` and lies on the line segment between `p₁` and `p₃`), then the angle at the third point `p₃`, with the angle's vertex at `p₂` and one leg extending to `p₁`, is zero. This theorem implies that if a point is strictly between two others, the line connecting the first and third point passes straight through the second point, forming an angle of zero degrees at the third point when viewed in reverse direction.
More concisely: If three points `p₁`, `p₂`, and `p₃` in a Euclidean space lie on the same line with `p₂` strictly between `p₁` and `p₃`, then the angle at `p₃` with vertex `p₂` and leg extending to `p₁` is zero.
|
EuclideanGeometry.angle_eq_of_ne
theorem EuclideanGeometry.angle_eq_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p p₀ : P}, p ≠ p₀ → EuclideanGeometry.angle p p₀ p = 0
The theorem `EuclideanGeometry.angle_eq_of_ne` states that in a Euclidean Geometry, given a normed add torsor over a vector space V, and a metric space P, if we have two distinct points `p` and `p₀`, then the angle formed by the line segments `pp₀p` (in which `p₀` is the vertex) is zero. In other words, the theorem says that the angle at a point is zero unless that point coincides with another point.
More concisely: In Euclidean geometry, the angle between two line segments with a common vertex and distinct endpoints is zero.
|
EuclideanGeometry.angle_const_vadd
theorem EuclideanGeometry.angle_const_vadd :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (v : V) (p₁ p₂ p₃ : P),
EuclideanGeometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
This theorem states that angles in Euclidean Geometry are invariant under translation. Specifically, given any three points `p₁`, `p₂`, `p₃` in a metric space `P`, and a vector `v` in a normed additively commutative group `V` with an inner product space over the reals, the angle at `p₂` between the line segments to `p₁` and `p₃` remains the same even when all the points are translated by the vector `v`. This invariance is a fundamental property of angles in Euclidean space.
More concisely: The angle between line segments connecting fixed points in a Euclidean space is invariant under translations.
|
EuclideanGeometry.angle_ne_pi_of_not_collinear
theorem EuclideanGeometry.angle_ne_pi_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ ≠ Real.pi
This theorem states that if three points are non-collinear (i.e., they do not all lie on the same straight line), then the angle they form, with the middle point as the vertex, is not equal to π (or 180 degrees in the Euclidean plane). In other words, the line segments connecting the vertex to the other two points do not form a straight line if the points do not all lie on the same line. The theorem applies in a vector space with a normed additivity group structure and an inner product space over the real numbers, and where distances can be measured, i.e., a metric space. The points are considered in a normed add-torsor, which is a set where you can subtract points to get a vector and add a vector to a point to get another point.
More concisely: In a normed additivity group with an inner product over the real numbers, three non-collinear points form angles less than π (180 degrees) with each other.
|
EuclideanGeometry.angle_add_const
theorem EuclideanGeometry.angle_add_const :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V),
EuclideanGeometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = EuclideanGeometry.angle v₁ v₂ v₃
The theorem `EuclideanGeometry.angle_add_const` states that the angles in a vector space are translation invariant. This means that if you translate (or shift) the vectors `v₁`, `v₂`, and `v₃` by a common vector `v`, the angle at `v₂` between the line segments to `v₁` and `v₃` remains the same as the original angle. This applies to any normed additively commutative group and inner product space over the real numbers.
More concisely: In a normed additively commutative group and inner product space over the real numbers, the angle between two vectors is invariant under translation.
|
EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi
theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_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] {p₁ p₂ p₃ : P},
Collinear ℝ {p₁, p₂, p₃} ↔
p₁ = p₂ ∨ p₃ = p₂ ∨ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
This theorem states that in Euclidean Geometry, three points are said to be collinear if and only if the first or third point is the same as the second point or the undirected angle between them is either 0 or \(\pi\) radians (\(180^{\circ}\)). In other words, three points lie on the same line if either two of them coincide or the angle between the segments connecting them is either straight (0 degrees or \(\pi\) radians) or flat (180 degrees or \(\pi\) radians).
More concisely: In Euclidean geometry, three points are collinear if and only if they either coincide or form a straight or flat angle between them.
|
EuclideanGeometry.angle_midpoint_eq_pi
theorem EuclideanGeometry.angle_midpoint_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] (p1 p2 : P),
p1 ≠ p2 → EuclideanGeometry.angle p1 (midpoint ℝ p1 p2) p2 = Real.pi
The theorem `EuclideanGeometry.angle_midpoint_eq_pi` states that for any two distinct points `p1` and `p2` in a Euclidean space, the angle ∠p1Mp2, where M is the midpoint of the line segment between `p1` and `p2`, is equal to π (the mathematical constant Pi, approximately 3.14159265). Here, the angle is measured in radians, with the midpoint as the vertex. The Euclidean space is modeled by an inner product space over the real numbers, with `V` being the type of vectors in the space, `P` the type of points, and the `NormedAddCommGroup`, `InnerProductSpace`, `MetricSpace`, and `NormedAddTorsor` structures providing the required operations and properties.
More concisely: The angle between two distinct points in a Euclidean space, measured from one point to the midpoint of the line segment connecting them, is equal to π radians.
|
EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi
theorem EuclideanGeometry.left_dist_ne_zero_of_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = Real.pi → dist p1 p2 ≠ 0
The theorem `EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi` states that in a Euclidean space, if the undirected angle at point B (denoted as `p2` in the code) between the line segments BA ( `p1` in the code) and BC ( `p3` in the code) is equal to π (equivalent to 180 degrees), then the distance between point A (`p1`) and point B (`p2`) is not zero. This essentially means that if the three points form a straight line (an angle of π), then points A and B cannot coincide.
More concisely: In a Euclidean space, if the angle between line segments connecting points `p1`, `p2`, and `p3` is equal to π, then the distance between `p1` and `p2` is non-zero.
|
EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq
theorem EuclideanGeometry.angle_left_midpoint_eq_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] {p1 p2 p3 : P},
dist p3 p1 = dist p3 p2 → EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p1 = Real.pi / 2
This theorem states that in Euclidean geometry, if we have three points A, B, and C, with M being the midpoint of the line segment AB, and the distance from C to A is the same as the distance from C to B, then the angle CMA (angle formed by points C, M, A) is equal to π/2 or 90 degrees.
More concisely: In Euclidean geometry, if point M is the midpoint of segment AB and AC = BC, then angle CMA equals π/2 (90 degrees).
|
EuclideanGeometry.angle_ne_zero_of_not_collinear
theorem EuclideanGeometry.angle_ne_zero_of_not_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] {p₁ p₂ p₃ : P},
¬Collinear ℝ {p₁, p₂, p₃} → EuclideanGeometry.angle p₁ p₂ p₃ ≠ 0
The given theorem, "EuclideanGeometry.angle_ne_zero_of_not_collinear", states that if three points are not collinear (i.e., they do not lie on the same straight line), then the angle formed at the second point by the line segments to the first and third points is not zero. Here, "Collinear ℝ {p₁, p₂, p₃}" checks if the points p₁, p₂, and p₃ are collinear by checking if the vector span of the points has a dimension of at most `1`, and "EuclideanGeometry.angle p₁ p₂ p₃" calculates the undirected angle at `p₂` between the line segments to `p₁` and `p₃`. If any of the points equal `p₂`, the angle is set as π/2. In the context of Euclidean Geometry, this theorem highlights an essential characteristic distinguishing non-collinear points.
More concisely: If three points in Euclidean space are not collinear, then the angle between the line segments connecting the first and second points and the second and third points is non-zero.
|
EuclideanGeometry.angle_le_pi
theorem EuclideanGeometry.angle_le_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] (p1 p2 p3 : P),
EuclideanGeometry.angle p1 p2 p3 ≤ Real.pi
This theorem states that in a Euclidean geometry setup, the angle at any point is always less than or equal to $\pi$. This setup involves a Normed Additive Commutative Group, an Inner Product Space over the Real numbers, a Metric Space, and a Normed Additive Torsor. The angle is measured at a point `p2` between the line segments from `p2` to `p1` and from `p2` to `p3`. The value of $\pi$ is defined as twice a zero of cosine in the interval [1, 2].
More concisely: In a Euclidean geometry setup, the angle between two line segments with a common endpoint measures less than or equal to $\pi$ radians.
|
EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi
theorem EuclideanGeometry.dist_eq_add_dist_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] {p1 p2 p3 : P},
p1 ≠ p2 → p3 ≠ p2 → (dist p1 p3 = dist p1 p2 + dist p3 p2 ↔ EuclideanGeometry.angle p1 p2 p3 = Real.pi)
This theorem, named `EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi`, states that for any three points `p1`, `p2`, and `p3` in a normed add torsor over a normed add commutative group structure with an inner product space, given that `p1` is not equal to `p2` and `p3` is not equal to `p2`, the distance from `p1` to `p3` equals the sum of the distance from `p1` to `p2` and the distance from `p3` to `p2` if and only if the angle at `p2` between the line segments to `p1` and `p3` equals π. In other words, the theorem connects the condition of straight-line (180-degree) angle between three points with the equality of the length of one side of the triangle formed by these points to the sum of the lengths of the other two sides.
More concisely: For points `p1`, `p2`, and `p3` in a normed add torsor over a normed add commutative group with an inner product space, the distance from `p1` to `p3` equals the sum of the distances from `p1` to `p2` and from `p2` to `p3` if and only if the angle at `p2` between the line segments to `p1` and `p3` is a right angle (180 degrees).
|
EuclideanGeometry.angle_const_sub
theorem EuclideanGeometry.angle_const_sub :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V),
EuclideanGeometry.angle (v - v₁) (v - v₂) (v - v₃) = EuclideanGeometry.angle v₁ v₂ v₃
This theorem states that the angles in a vector space are invariant to inversion. In other words, for any vector `v` and any three other vectors `v₁`, `v₂`, and `v₃` in a vector space equipped with a normed add commutative group structure and an inner product space over the real numbers, the angle at `v` between the line segments to `v₁`, `v₂`, and `v₃` is the same as the angle at `v₁` between the line segments to `v`, `v₂`, and `v₃`. This implies that changing the order or direction of the vectors does not change the angle between them.
More concisely: The angle between any three vectors in a normed add commutative group and inner product space over the real numbers is invariant under inversion.
|
EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero
theorem EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_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] {p₁ p₂ p₃ : P},
Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ (EuclideanGeometry.angle p₁ p₂ p₃).sin = 0
This theorem states that for any three points (p₁, p₂, p₃) in a Euclidean space, the three points are collinear (i.e., they lie on the same straight line) if and only if either the first point equals the second, the third point equals the second, or the sine of the angle between the three points is zero. The angle is defined as the undirected angle at the second point (p₂) between the line segments towards the first point (p₁) and the third point (p₃). If either the first or third point equals the second point, the angle is defined as π/2.
More concisely: In a Euclidean space, three points are collinear if and only if they form a straight angle (i.e., the sine of the angle between the line segments towards them is zero), except when two points are identical in which case the angle is considered to be π/2.
|
EuclideanGeometry.angle_vsub_const
theorem EuclideanGeometry.angle_vsub_const :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ p : P),
EuclideanGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = EuclideanGeometry.angle p₁ p₂ p₃
The theorem `EuclideanGeometry.angle_vsub_const` states that angles in Euclidean geometry are invariant under translation. Specifically, given any four points `p₁`, `p₂`, `p₃`, and `p` in a metric space with a normed add torsor structure, the angle at `p` between the line segments to `p₁`, `p₂`, and `p₃` is equal to the original angle between `p₁`, `p₂`, and `p₃`. This essentially means that if we "move" the entire shape in the space without altering its orientation, the angles between any three points will remain the same.
More concisely: In a metric space with a normed add torsor structure, the angle between any three points is invariant under translation.
|
EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two
theorem EuclideanGeometry.sin_eq_one_iff_angle_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).sin = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
The theorem `EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two` states that for any three points `p₁`, `p₂` and `p₃` in a Euclidean space, the sine of the angle at `p₂` between the line segments to `p₁` and `p₃` is equal to 1 if and only if the said angle is equal to π / 2 (which is equivalent to a right angle or 90 degrees). This theorem applies to any space that is equipped with the structures of a `NormedAddCommGroup`, an `InnerProductSpace` over the reals, a `MetricSpace` and a `NormedAddTorsor`.
More concisely: In a Euclidean space equipped with the structures of a NormedAddCommGroup, an InnerProductSpace over the reals, a MetricSpace, and a NormedAddTorsor, the sine of the angle between two line segments is equal to 1 if and only if the angle is a right angle (π/2 radians).
|
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left
theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = Real.pi → EuclideanGeometry.angle p2 p1 p3 = 0
This theorem states that in Euclidean geometry, given any three points A, B, and C where B is the vertex, if the angle ∠ABC (angle between line segment AB and BC) is pi (π, i.e., 180 degrees), then the angle ∠BAC (angle between line segment BA and AC) is 0. In other words, if the line segments AB and BC are in a straight line, then A, B, and C are collinear and the angle at A looking towards B and then C is zero. This theorem holds for any normed additive commutative group, inner product space, metric space, and normed additive torsor.
More concisely: In any normed additive commutative group, inner product space, metric space, or normed additive torsor, if the angle between line segments AB and BC is π (180 degrees), then the angle between BA and AC is 0, making A, B, and C collinear.
|
EuclideanGeometry.angle_eq_right
theorem EuclideanGeometry.angle_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] (p₀ p : P),
EuclideanGeometry.angle p p₀ p₀ = Real.pi / 2
This theorem, named `EuclideanGeometry.angle_eq_right`, states that for any point `p` in a Euclidean space with normed add torsor structure, the angle formed by the line segment from `p` to another point `p₀` and the line segment from `p₀` to itself, denoted as ∠`pp₀p₀`, is always equal to π/2 (or, in everyday terms, a right angle). The underlying space is equipped with an inner product and normed additive commutative group structure.
More concisely: In a Euclidean space with normed additive commutative group structure and inner product, the angle between the line segment from a point to itself and the line segment connecting that point to another point is always a right angle (equal to π/2 radians).
|
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi
theorem EuclideanGeometry.angle_eq_angle_of_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] (p1 : P) {p2 p3 p4 : P},
EuclideanGeometry.angle p2 p3 p4 = Real.pi →
EuclideanGeometry.angle p1 p2 p3 = EuclideanGeometry.angle p1 p2 p4
This theorem states that in a Euclidean space, if the angle at point C formed by points B and D (denoted as ∠BCD) is equal to π (180 degrees), then the angle at point B formed by points A and C (denoted as ∠ABC) is equal to the angle at point B formed by points A and D (denoted as ∠ABD). In other words, if a straight line (BCD) is formed in a Euclidean space, then the angles subtended by the line segments with the same endpoint (ABC and ABD) are equal.
More concisely: In a Euclidean space, if the angle formed by points B and D is π radians (180 degrees), then the angles formed by point B with points A and C, and angles formed by point B with points A and D, are equal.
|
Sbtw.angle₃₂₁_eq_pi
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi
The theorem `Sbtw.angle₃₂₁_eq_pi` states that if in a three-point configuration, the second point is strictly between the first and the third point (in the real numbers), then the angle at the second point (when considered in reverse order, i.e., from the third to the second to the first point) is equal to π. Here, the angle is defined in terms of the Euclidean geometry angle, which is based on the inner product space with real numbers. The point being strictly between the other two is defined in terms of the Wbtw condition and the condition that the second point is distinct from the first and third points.
More concisely: If points $1$, $2$, and $3$ form a three-point configuration in the real numbers with $2$ strictly between $1$ and $3$, then the angle at $2$ (from $3$ to $2$ to $1$) is equal to $\pi$.
|
Sbtw.angle₂₁₃_eq_zero
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₂ p₁ p₃ = 0
The theorem `Sbtw.angle₂₁₃_eq_zero` states that for any three points `p₁`, `p₂`, and `p₃` in a Euclidean space, if the second point `p₂` is strictly between the first `p₁` and third `p₃` point, then the angle at `p₁` formed by the line segments `p₁p₂` and `p₁p₃` is zero. This is to say, in such a scenario, the line segments `p₁p₂` and `p₁p₃` are collinear, forming a straight line.
More concisely: If points `p₁`, `p₂`, and `p₃` in a Euclidean space are such that `p₂` is strictly between `p₁` and `p₃`, then the angle between line segments `p₁p₂` and `p₁p₃` is equal to 0 degrees.
|
Sbtw.angle₂₃₁_eq_zero
theorem Sbtw.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] {p₁ p₂ p₃ : P},
Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₂ p₃ p₁ = 0
This theorem states that given three points - p₁, p₂, and p₃ - if the point p₂ is strictly between p₁ and p₃, then the angle at point p₃, formed by the line segments p₃p₁ and p₃p₂, is zero. Here, strictly between means that p₂ is not equal to either p₁ or p₃ and falls on the line segment formed by p₁ and p₃. The theorem is applicable in any normed add commutative group with an inner product space over real numbers and a normed add torsor, which provides a metric space structure.
More concisely: Given three points p₁, p₂, and p₃ in a normed add commutative group with an inner product space over real numbers and a normed add torsor, if p₂ is strictly between p₁ and p₃, then the angle at p₃ between the line segments p₃p₁ and p₃p₂ is 0.
|
EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two
theorem EuclideanGeometry.cos_eq_zero_iff_angle_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).cos = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
This theorem states that in the context of Euclidean Geometry, the cosine of the angle formed by three points equals zero if and only if the angle is equal to π/2 radians (or 90 degrees). Specifically, the angle is being taken at the second point, formed by the line segment to the first point and the line segment to the third point. If any of the points coincide, the angle is defined to be π/2. This theorem is applicable in any normed add torsor over a metric space with an inner product.
More concisely: In the context of Euclidean Geometry and a normed additive torsor over a metric space with an inner product, the cosine of the angle between two line segments is 0 if and only if the angle is a right angle (equal to 90 degrees or π/2 radians).
|
EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi
theorem EuclideanGeometry.cos_eq_neg_one_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] {p₁ p₂ p₃ : P},
(EuclideanGeometry.angle p₁ p₂ p₃).cos = -1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
This theorem states that in Euclidean geometry, for any three points defined over a normed addition group and inner product space, the cosine of the angle formed by these three points is -1 if and only if the actual angle is equal to π (pi). Here, the angle is defined as the undirected angle at the second point between the line segments to the first and third points. The value of π is defined as twice the zero of cosine in the interval [1,2].
More concisely: In Euclidean geometry, the cosine of the undirected angle between three points in a normed addition group and inner product space is -1 if and only if the angle is equal to π (pi), where π is defined as twice the zero of cosine.
|
EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi
theorem EuclideanGeometry.dist_eq_add_dist_of_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = Real.pi → dist p1 p3 = dist p1 p2 + dist p3 p2
The theorem, `EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi`, states that in the context of Euclidean geometry, if the angle formed at point B by lines BA and BC (denoted as ∠ABC) is equal to π (180 degrees), then the length of the line segment AC (denoted as dist A C) is equal to the sum of the lengths of the line segments AB and BC (denoted as dist A B and dist B C respectively). This corresponds to the geometric property that in a straight line (angle of π), the length of the entire line is equal to the sum of its parts.
More concisely: In Euclidean geometry, if angle ∠ABC between lines BA and BC is equal to 180 degrees (π radians), then the length of segment AC is equal to the sum of the lengths of segments AB and BC.
|
EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq
theorem EuclideanGeometry.angle_right_midpoint_eq_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] {p1 p2 p3 : P},
dist p3 p1 = dist p3 p2 → EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p2 = Real.pi / 2
This theorem states that in a Euclidean geometry, if we have three points A, B, and C represented by `p1`, `p2`, and `p3` respectively, and M is the midpoint of segment AB, then if the distance from C to A is the same as the distance from C to B (`dist p3 p1 = dist p3 p2`), the angle ∠CMB (`EuclideanGeometry.angle p3 (midpoint ℝ p1 p2) p2`) is equal to π / 2 (`Real.pi / 2`). In other words, the angle at the midpoint of a segment, formed by a point that is equidistant from each endpoint of the segment, is a right angle (90 degrees or π/2 radians).
More concisely: In Euclidean geometry, if point C is equidistant from points A and B, then angle CMB formed by points C, M (midpoint of AB), and B is a right angle (π/2 radians).
|
EuclideanGeometry.angle_vadd_const
theorem EuclideanGeometry.angle_vadd_const :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] (v₁ v₂ v₃ : V) (p : P),
EuclideanGeometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = EuclideanGeometry.angle v₁ v₂ v₃
This theorem, known as "EuclideanGeometry.angle_vadd_const", states that angles in Euclidean Geometry are translation invariant. This means that the angle at a point `p` between three vectors `v₁`, `v₂`, `v₃` remains the same even when the point is translated in space. That is, if we add another point `p` to each of the vectors, the resulting angle between the translated vectors is still the same as the original angle between `v₁`, `v₂`, `v₃`. It is an application of the universal property of angles in a Euclidean space. The theorem is a fundamental concept in Euclidean Geometry and it is crucial for various geometrical proofs and constructions.
More concisely: The angle between three vectors in Euclidean geometry is unchanged when the vectors are translated by the same point.
|
EuclideanGeometry.angle_sub_const
theorem EuclideanGeometry.angle_sub_const :
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V),
EuclideanGeometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = EuclideanGeometry.angle v₁ v₂ v₃
This theorem states that angles in a vector space are translation invariant. In other words, if you have three vectors `v₁`, `v₂`, and `v₃` in a vector space with a normed add commutative group and an inner product space structure over the real numbers, then subtracting a constant vector `v` from each of `v₁`, `v₂`, and `v₃` does not change the angle between them. This reflects the geometric intuition that moving a figure around in space without rotating or resizing it does not change its internal angles.
More concisely: In a normed additive commutative group and inner product space over the real numbers, the angle between two vectors is invariant under translation.
|
Wbtw.angle₃₁₂_eq_zero_of_ne
theorem Wbtw.angle₃₁₂_eq_zero_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₁ → EuclideanGeometry.angle p₃ p₁ p₂ = 0
This theorem states that given three points wherein the second point is weakly between the first and the third, and the second point is not equal to the first, then the angle at the first point when considering the line segments to the second and third points (in reverse order) is zero. In other words, if we have points `p₁`, `p₂`, and `p₃`, with `p₂` weakly between `p₁` and `p₃` and distinct from `p₁`, then the angle formed at point `p₁` by the segments `p₃p₁` and `p₁p₂` is zero degrees. This essentially means that the three points lie on the same straight line with `p₂` in between `p₁` and `p₃`.
More concisely: Given distinct points `p₁`, `p₂`, and `p₃` with `p₂` weakly between `p₁` and `p₃`, the angle at `p₁` formed by the line segments `p₁p₂` and `p₂p₃` is zero degrees.
|
Wbtw.angle₂₁₃_eq_zero_of_ne
theorem Wbtw.angle₂₁₃_eq_zero_of_ne :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
[inst_2 : MetricSpace P] [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
Wbtw ℝ p₁ p₂ p₃ → p₂ ≠ p₁ → EuclideanGeometry.angle p₂ p₁ p₃ = 0
This theorem states that, given three points where the second point is weakly between the other two and is not equal to the first point, the angle at the first point is zero. In other words, if you have three points where the second point is not only on the line segment between the other two but also closer to the third point, and also it is distinct from the first point, then the angle formed at the first point will be zero. This implies that the three points are collinear with the first point being the endpoint of the line segment.
More concisely: Given three distinct points on a line, if the second point lies between the first and third points and is closer to the third point, then the angle at the first point is zero, implying the points are collinear.
|
EuclideanGeometry.angle_const_vsub
theorem EuclideanGeometry.angle_const_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] (p p₁ p₂ p₃ : P),
EuclideanGeometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
This theorem, named `EuclideanGeometry.angle_const_vsub`, states that angles in Euclidean geometry are translation invariant. More specifically, for any four points `p`, `p₁`, `p₂`, and `p₃` in a metric space `P`, the angle at `p` between the line segments to `p₁`, `p₂`, and `p₃` is equal to the angle at `p₂` between the line segments to `p₁`, `p`, and `p₃`. This means if we translate (or shift) the entire configuration of points in the space, the measured angle does not change.
More concisely: In Euclidean geometry, the angle between line segments from points `p`, `p₁`, and `p₂`, and from points `p₂`, `p₁`, and `p₃` is equal.
|
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right
theorem EuclideanGeometry.angle_eq_zero_of_angle_eq_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] {p1 p2 p3 : P},
EuclideanGeometry.angle p1 p2 p3 = Real.pi → EuclideanGeometry.angle p2 p3 p1 = 0
The theorem `EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right` states that given the setup of a vector space V and a metric space P, if we have three points p1, p2, p3 in P, and the undirected angle at p2 between the line segments to p1 and p3 is π (or 180 degrees), then the angle at p3 between the line segments to p2 and p1 is 0 (a straight line). In terms of plane geometry, if angle ABC is a straight angle, then angle BCA forms a straight line.
More concisely: If the undirected angle between two line segments is a straight angle (π radians or 180 degrees), then the corresponding alternate angles are equal and form a linear chain, i.e., their measures sum up to 180 degrees or π radians.
|
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi
theorem EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_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] {p1 p2 p3 p4 p5 : P},
EuclideanGeometry.angle p1 p5 p3 = Real.pi →
EuclideanGeometry.angle p2 p5 p4 = Real.pi →
EuclideanGeometry.angle p1 p5 p2 = EuclideanGeometry.angle p3 p5 p4
The theorem, known as the **Vertical Angles Theorem**, states that if two straight lines intersect each other at a point, then the angles opposite each other (vertical angles) are equal. More specifically, given five points `p1`, `p2`, `p3`, `p4`, `p5` in a Euclidean space with a specified normed add torsor and inner product space, if the angle formed by `p1`, `p5`, `p3` and the angle formed by `p2`, `p5`, `p4` are both equal to $\pi$ (i.e., they are both straight angles), then the angle formed by `p1`, `p5`, `p2` is equal to the angle formed by `p3`, `p5`, `p4`. This theorem is a fundamental property of Euclidean geometry.
More concisely: In a Euclidean space with given norm and inner product, if two lines intersect and the angles formed by the intersection point with the lines on either side are both right angles, then the angles are congruent.
|