Loogle!

Result

Found 187 declarations mentioning EuclideanGeometry.angle.

EuclideanGeometry.angle 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : ℝ
EuclideanGeometry.angle_le_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi
EuclideanGeometry.angle_nonneg 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : 0 ≤ EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_self_of_ne 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p p₀ : P} (h : p ≠ p₀) : EuclideanGeometry.angle p p₀ p = 0
EuclideanGeometry.angle_comm 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₃ p₂ p₁
EuclideanGeometry.left_dist_ne_zero_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : dist p₁ p₂ ≠ 0
EuclideanGeometry.right_dist_ne_zero_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : dist p₃ p₂ ≠ 0
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_left 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : EuclideanGeometry.angle p₂ p₁ p₃ = 0
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : EuclideanGeometry.angle p₂ p₃ p₁ = 0
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P} (h : EuclideanGeometry.angle p₂ p₃ p₄ = Real.pi) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄
EuclideanGeometry.cos_eq_neg_one_iff_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = -1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
EuclideanGeometry.cos_eq_one_iff_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0
EuclideanGeometry.angle_self_left 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ p : P) : EuclideanGeometry.angle p₀ p₀ p = Real.pi / 2
EuclideanGeometry.angle_self_right 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₀ p : P) : EuclideanGeometry.angle p p₀ p₀ = Real.pi / 2
EuclideanGeometry.angle_add_angle_eq_pi_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P} (h : EuclideanGeometry.angle p₂ p₃ p₄ = Real.pi) : EuclideanGeometry.angle p₁ p₃ p₂ + EuclideanGeometry.angle p₁ p₃ p₄ = Real.pi
EuclideanGeometry.dist_eq_add_dist_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂
EuclideanGeometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ p₅ : P} (hapc : EuclideanGeometry.angle p₁ p₅ p₃ = Real.pi) (hbpd : EuclideanGeometry.angle p₂ p₅ p₄ = Real.pi) : EuclideanGeometry.angle p₁ p₅ p₂ = EuclideanGeometry.angle p₃ p₅ p₄
Sbtw.angle₁₂₃_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
Sbtw.angle₃₂₁_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi
EuclideanGeometry.angle_eq_pi_iff_sbtw 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi ↔ Sbtw ℝ p₁ p₂ p₃
EuclideanGeometry.sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0 ∨ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
Sbtw.angle₁₃₂_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₁ p₃ p₂ = 0
Sbtw.angle₂₁₃_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₂ p₁ p₃ = 0
Sbtw.angle₂₃₁_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₂ p₃ p₁ = 0
Sbtw.angle₃₁₂_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : EuclideanGeometry.angle p₃ p₁ p₂ = 0
EuclideanGeometry.dist_eq_abs_sub_dist_of_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = 0) : dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|
EuclideanGeometry.dist_eq_add_dist_iff_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) : dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
Wbtw.angle₁₃₂_eq_zero_of_ne 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₃ : p₂ ≠ p₃) : EuclideanGeometry.angle p₁ p₃ p₂ = 0
Wbtw.angle₂₁₃_eq_zero_of_ne 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) : EuclideanGeometry.angle p₂ p₁ p₃ = 0
Wbtw.angle₂₃₁_eq_zero_of_ne 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₃ : p₂ ≠ p₃) : EuclideanGeometry.angle p₂ p₃ p₁ = 0
Wbtw.angle₃₁₂_eq_zero_of_ne 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Wbtw ℝ p₁ p₂ p₃) (hp₂p₁ : p₂ ≠ p₁) : EuclideanGeometry.angle p₃ p₁ p₂ = 0
Sbtw.angle_eq_left 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p p₂ : P} (p₃ : P) (h : Sbtw ℝ p₂ p₁ p) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p p₂ p₃
Sbtw.angle_eq_right 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₂ p₃ p : P} (p₁ : P) (h : Sbtw ℝ p₂ p₃ p) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p
EuclideanGeometry.cos_eq_zero_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Real.cos (EuclideanGeometry.angle p₁ p₂ p₃) = 0 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
EuclideanGeometry.sin_eq_one_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 1 ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
Wbtw.angle_eq_left 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p p₂ : P} (p₃ : P) (h : Wbtw ℝ p₂ p₁ p) (hp₁p₂ : p₁ ≠ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p p₂ p₃
Wbtw.angle_eq_right 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₂ p₃ p : P} (p₁ : P) (h : Wbtw ℝ p₂ p₃ p) (hp₃p₂ : p₃ ≠ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p
EuclideanGeometry.angle_midpoint_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ : P) (hp₁p₂ : p₁ ≠ p₂) : EuclideanGeometry.angle p₁ (midpoint ℝ p₁ p₂) p₂ = Real.pi
EuclideanGeometry.angle_neg 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ v₂ v₃ : V) : EuclideanGeometry.angle (-v₁) (-v₂) (-v₃) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.collinear_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi) : Collinear ℝ {p₁, p₂, p₃}
EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) : dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0
EuclideanGeometry.angle_ne_pi_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : EuclideanGeometry.angle p₁ p₂ p₃ ≠ Real.pi
EuclideanGeometry.angle_lt_pi_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi
EuclideanGeometry.angle_const_sub 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V) : EuclideanGeometry.angle (v - v₁) (v - v₂) (v - v₃) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.angle_sub_const 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V) : EuclideanGeometry.angle (v₁ - v) (v₂ - v) (v₃ - v) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.collinear_of_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = 0) : Collinear ℝ {p₁, p₂, p₃}
EuclideanGeometry.angle_ne_zero_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : EuclideanGeometry.angle p₁ p₂ p₃ ≠ 0
EuclideanGeometry.collinear_of_sin_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0) : Collinear ℝ {p₁, p₂, p₃}
EuclideanGeometry.angle_pos_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : 0 < EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.sin_ne_zero_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) ≠ 0
EuclideanGeometry.sin_pos_of_not_collinear 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : 0 < Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.angle_add_const 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v₁ v₂ v₃ v : V) : EuclideanGeometry.angle (v₁ + v) (v₂ + v) (v₃ + v) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.angle_const_add 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (v v₁ v₂ v₃ : V) : EuclideanGeometry.angle (v + v₁) (v + v₂) (v + v₃) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.collinear_iff_eq_or_eq_or_sin_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : Collinear ℝ {p₁, p₂, p₃} ↔ p₁ = p₂ ∨ p₃ = p₂ ∨ Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) = 0
EuclideanGeometry.collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [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
EuclideanGeometry.angle_const_vsub 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p p₁ p₂ p₃ : P) : EuclideanGeometry.angle (p -ᵥ p₁) (p -ᵥ p₂) (p -ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_vsub_const 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ p : P) : EuclideanGeometry.angle (p₁ -ᵥ p) (p₂ -ᵥ p) (p₃ -ᵥ p) = EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_eq_zero_iff_eq_and_ne_or_sbtw 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [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₁
EuclideanGeometry.angle_eq_zero_iff_ne_and_wbtw 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [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₁
EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : dist p₃ p₁ = dist p₃ p₂) : EuclideanGeometry.angle p₃ (midpoint ℝ p₁ p₂) p₁ = Real.pi / 2
EuclideanGeometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : dist p₃ p₁ = dist p₃ p₂) : EuclideanGeometry.angle p₃ (midpoint ℝ p₁ p₂) p₂ = Real.pi / 2
EuclideanGeometry.continuousAt_angle 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {x : P × P × P} (hx12 : x.1 ≠ x.2.1) (hx32 : x.2.2 ≠ x.2.1) : ContinuousAt (fun y => EuclideanGeometry.angle y.1 y.2.1 y.2.2) x
EuclideanGeometry.angle_smul_left_of_pos 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₄ : P} (p₃ : P) {r : ℝ} (hr : 0 < r) (hrv : r • (p₄ -ᵥ p₂) = p₁ -ᵥ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₂ p₃
EuclideanGeometry.angle_smul_right_of_pos 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ : P) {p₂ p₃ p₄ : P} {r : ℝ} (hr : 0 < r) (hrv : r • (p₄ -ᵥ p₂) = p₃ -ᵥ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄
EuclideanGeometry.angle_const_vadd 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v : V) (p₁ p₂ p₃ : P) : EuclideanGeometry.angle (v +ᵥ p₁) (v +ᵥ p₂) (v +ᵥ p₃) = EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_vadd_const 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (v₁ v₂ v₃ : V) (p : P) : EuclideanGeometry.angle (v₁ +ᵥ p) (v₂ +ᵥ p) (v₃ +ᵥ p) = EuclideanGeometry.angle v₁ v₂ v₃
EuclideanGeometry.angle_pointReflection_right 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : EuclideanGeometry.angle p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₃) = Real.pi - EuclideanGeometry.angle p₁ p₂ p₃
AffineIsometry.angle_map 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂] [MetricSpace P₂] [NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ] P₂) (p₁ p₂ p₃ : P) : EuclideanGeometry.angle (f p₁) (f p₂) (f p₃) = EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_homothety 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p p₁ p₂ p₃ : P) {r : ℝ} (h : r ≠ 0) : EuclideanGeometry.angle ((AffineMap.homothety p r) p₁) ((AffineMap.homothety p r) p₂) ((AffineMap.homothety p r) p₃) = EuclideanGeometry.angle p₁ p₂ p₃
AffineSubspace.angle_coe 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : AffineSubspace ℝ P} (p₁ p₂ p₃ : ↥s) : EuclideanGeometry.angle ↑p₁ ↑p₂ ↑p₃ = EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.oangle_eq_pi_iff_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑Real.pi ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi
EuclideanGeometry.cos_oangle_eq_cos_angle 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : (EuclideanGeometry.oangle p₁ p p₂).cos = Real.cos (EuclideanGeometry.angle p₁ p p₂)
EuclideanGeometry.angle_eq_abs_oangle_toReal 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.angle p₁ p p₂ = |(EuclideanGeometry.oangle p₁ p p₂).toReal|
EuclideanGeometry.oangle_eq_angle_of_sign_eq_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1) : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.oangle_eq_zero_iff_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ = 0 ↔ EuclideanGeometry.angle p₁ p p₂ = 0
EuclideanGeometry.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P} (h : (EuclideanGeometry.oangle p₁ p p₂).sign = 0) : p₁ = p ∨ p₂ = p ∨ EuclideanGeometry.angle p₁ p p₂ = 0 ∨ EuclideanGeometry.angle p₁ p p₂ = Real.pi
EuclideanGeometry.oangle_eq_neg_angle_of_sign_eq_neg_one 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1) : EuclideanGeometry.oangle p₁ p₂ p₃ = -↑(EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.oangle_eq_angle_or_eq_neg_angle 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p p₁ p₂ : P} (hp₁ : p₁ ≠ p) (hp₂ : p₂ ≠ p) : EuclideanGeometry.oangle p₁ p p₂ = ↑(EuclideanGeometry.angle p₁ p p₂) ∨ EuclideanGeometry.oangle p₁ p p₂ = -↑(EuclideanGeometry.angle p₁ p p₂)
EuclideanGeometry.oangle_eq_of_angle_eq_of_sign_eq 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆) (hs : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₄ p₅ p₆).sign) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2)) : EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
EuclideanGeometry.angle_eq_pi_div_two_of_oangle_eq_neg_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
EuclideanGeometry.angle_rev_eq_pi_div_two_of_oangle_eq_neg_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(-Real.pi / 2)) : EuclideanGeometry.angle p₃ p₂ p₁ = Real.pi / 2
EuclideanGeometry.angle_eq_iff_oangle_eq_of_sign_eq 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (hp₄ : p₄ ≠ p₅) (hp₆ : p₆ ≠ p₅) (hs : (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₆
EuclideanGeometry.oangle_eq_neg_of_angle_eq_of_sign_eq_neg 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆) (hs : (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -(EuclideanGeometry.oangle p₄ p₅ p₆).sign) : EuclideanGeometry.oangle p₁ p₂ p₃ = -EuclideanGeometry.oangle p₄ p₅ p₆
EuclideanGeometry.oangle_eq_or_eq_neg_of_angle_eq 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₄ p₅ p₆) (h1 : p₂ ≠ p₁) (h2 : p₂ ≠ p₃) (h3 : p₅ ≠ p₄) (h4 : p₅ ≠ p₆) : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₄ p₅ p₆ ∨ EuclideanGeometry.oangle p₁ p₂ p₃ = -EuclideanGeometry.oangle p₄ p₅ p₆
EuclideanGeometry.angle_eq_iff_oangle_eq_neg_of_sign_eq_neg 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (hp₄ : p₄ ≠ p₅) (hp₆ : p₆ ≠ p₅) (hs : (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₆
EuclideanGeometry.two_mul_angle_eq_abs_two_zsmul_oangle_toReal 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (h : EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi / 2) : 2 * EuclideanGeometry.angle p₁ p₂ p₃ = |(2 • EuclideanGeometry.oangle p₁ p₂ p₃).toReal|
EuclideanGeometry.angle_eq_iff_oangle_eq_or_wbtw 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (hp₁ : p₁ ≠ p₂) (hp₄ : p₄ ≠ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₃ p₂ p₄ ↔ EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
EuclideanGeometry.two_mul_angle_eq_two_pi_sub_abs_two_zsmul_oangle_toReal 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (hp₁ : p₁ ≠ p₂) (hp₃ : p₃ ≠ p₂) (h : Real.pi / 2 ≤ EuclideanGeometry.angle p₁ p₂ p₃) : 2 * EuclideanGeometry.angle p₁ p₂ p₃ = 2 * Real.pi - |(2 • EuclideanGeometry.oangle p₁ p₂ p₃).toReal|
EuclideanGeometry.angle_eq_angle_div_two_of_oangle_eq_of_sSameSide 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h₁₂ : p₁ ≠ p₂) (ha : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄) (hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₂ p₄ / 2
EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h₁₂ : p₁ ≠ p₂) (ha : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄) (hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi - EuclideanGeometry.angle p₁ p₂ p₄ / 2
EuclideanGeometry.angle_eq_angle_add_pi_div_two_of_oangle_eq_add_pi_of_sSameSide 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h₁₂ : p₁ ≠ p₂) (ha : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ + ↑Real.pi) (hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄) : EuclideanGeometry.angle p₁ p₂ p₃ = (EuclideanGeometry.angle p₁ p₂ p₄ + Real.pi) / 2
EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_add_pi_of_sOppSide 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ : P} (h₁₂ : p₁ ≠ p₂) (ha : EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ + ↑Real.pi) (hs : line[ℝ, p₁, p₂].SOppSide p₃ p₄) : EuclideanGeometry.angle p₁ p₂ p₃ = (Real.pi - EuclideanGeometry.angle p₁ p₂ p₄) / 2
EuclideanGeometry.angle_pos_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : 0 < EuclideanGeometry.angle p₂ p₃ p₁
EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
EuclideanGeometry.sin_angle_mul_dist_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : EuclideanGeometry.angle p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
EuclideanGeometry.cos_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
EuclideanGeometry.tan_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
EuclideanGeometry.angle_le_pi_div_two_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : EuclideanGeometry.angle p₂ p₃ p₁ ≤ Real.pi / 2
EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₃ ≠ p₂) : EuclideanGeometry.angle p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
EuclideanGeometry.angle_lt_pi_div_two_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₃ ≠ p₂) : EuclideanGeometry.angle p₂ p₃ p₁ < Real.pi / 2
EuclideanGeometry.tan_angle_mul_dist_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : EuclideanGeometry.angle p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ = p₂ ∨ p₃ ≠ p₂) : dist p₃ p₂ / Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₃
EuclideanGeometry.dist_div_sin_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₃
EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ = p₂) : dist p₁ p₂ / Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₃ p₂
EuclideanGeometry.sin_angle_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂) : Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
EuclideanGeometry.dist_sq_add_dist_sq_le_dist_sq_iff_pi_div_two_le_angle 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ≤ dist p₁ p₃ * dist p₁ p₃ ↔ Real.pi / 2 ≤ EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.dist_sq_eq_dist_mul_dist_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ : P} (hf : Sbtw ℝ p₁ p₄ p₃) (hc : EuclideanGeometry.angle p₁ p₄ p₂ = Real.pi / 2) (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : dist p₂ p₄ ^ 2 = dist p₁ p₄ * dist p₃ p₄
EuclideanGeometry.dist_sq_eq_dist_mul_dist_of_angle_eq_pi_div_two' 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ : P} (hf : Sbtw ℝ p₁ p₄ p₃) (hc : EuclideanGeometry.angle p₁ p₄ p₂ = Real.pi / 2) (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : dist p₁ p₂ ^ 2 = dist p₁ p₃ * dist p₁ p₄
EuclideanGeometry.dist_sq_eq_dist_mul_dist_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ : P} (hf : Sbtw ℝ p₁ p₄ p₃) (hc : EuclideanGeometry.angle p₁ p₄ p₂ = Real.pi / 2) : dist p₂ p₄ ^ 2 = dist p₁ p₄ * dist p₃ p₄ ↔ EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2
EuclideanGeometry.abs_oangle_toReal_lt_pi_div_two_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : |(EuclideanGeometry.oangle p₂ p₃ p₁).toReal| < Real.pi / 2
EuclideanGeometry.oangle_eq_oangle_of_two_zsmul_eq_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 • EuclideanGeometry.oangle p₂ p₃ p₁ = 2 • EuclideanGeometry.oangle p₅ p₆ p₄) (h₁₂₃ : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h₄₅₆ : EuclideanGeometry.angle p₄ p₅ p₆ = Real.pi / 2) : EuclideanGeometry.oangle p₂ p₃ p₁ = EuclideanGeometry.oangle p₅ p₆ p₄
EuclideanGeometry.oangle_eq_oangle_rev_of_two_zsmul_eq_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [Module.Oriented ℝ V (Fin 2)] {p₁ p₂ p₃ p₄ p₅ p₆ : P} (h : 2 • EuclideanGeometry.oangle p₂ p₃ p₁ = 2 • EuclideanGeometry.oangle p₄ p₆ p₅) (h₁₂₃ : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) (h₄₅₆ : EuclideanGeometry.angle p₄ p₅ p₆ = Real.pi / 2) : EuclideanGeometry.oangle p₂ p₃ p₁ = EuclideanGeometry.oangle p₄ p₆ p₅
EuclideanGeometry.angle_orthogonalProjection_self 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p : P) {p' : P} {s : AffineSubspace ℝ P} [s.direction.HasOrthogonalProjection] (h : p' ∈ s) : EuclideanGeometry.angle p' (↑((EuclideanGeometry.orthogonalProjection s) p)) p = Real.pi / 2
EuclideanGeometry.angle_self_orthogonalProjection 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p : P) {p' : P} {s : AffineSubspace ℝ P} [s.direction.HasOrthogonalProjection] (h : p' ∈ s) : EuclideanGeometry.angle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = Real.pi / 2
EuclideanGeometry.dist_orthogonalProjection_eq_iff_angle_eq 📋 Mathlib.Geometry.Euclidean.Angle.Bisector
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} [s₁.direction.HasOrthogonalProjection] [s₂.direction.HasOrthogonalProjection] (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂) : dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) = dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p) ↔ EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₁) p) = EuclideanGeometry.angle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p)
Affine.Triangle.angle_incenter 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.incenter t) = EuclideanGeometry.angle (Affine.Simplex.incenter t) (t.points i₁) (t.points i₃)
Affine.Triangle.two_mul_angle_incenter 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.incenter t) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃)
Affine.Triangle.angle_incenter_eq_angle_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.incenter t) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃) / 2
Affine.Triangle.angle_excenter_singleton 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t {i₁}) = EuclideanGeometry.angle (Affine.Simplex.excenter t {i₁}) (t.points i₁) (t.points i₃)
Affine.Triangle.two_mul_angle_excenter_singleton 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃)
Affine.Triangle.angle_excenter_singleton_eq_angle_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₂) (t.points i₁) (t.points i₃) / 2
Affine.Triangle.two_mul_angle_excenter_singleton_eq_angle_add_pi 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Affine.Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃) + Real.pi
Affine.Triangle.two_mul_angle_excenter_singleton_eq_pi_sub_angle 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : 2 * EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Affine.Simplex.excenter t {i₁}) = Real.pi - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (t.points i₁)
Affine.Triangle.angle_excenter_singleton_eq_angle_add_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Affine.Simplex.excenter t {i₁}) = (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃) + Real.pi) / 2
Affine.Triangle.angle_excenter_singleton_eq_pi_sub_angle_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Affine.Simplex.excenter t {i₁}) = (Real.pi - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (t.points i₁)) / 2
Affine.Triangle.angle_excenter_singleton_sub 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (t.points i₁) (t.points i₂) (Affine.Simplex.excenter t {i₁}) - EuclideanGeometry.angle (t.points i₃) (t.points i₂) (Affine.Simplex.excenter t {i₁}) = EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)
Affine.Simplex.ExcenterExists.angle_excenter_touchpoint_eq 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))} (h : s.ExcenterExists signs) {p : P} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₁) = EuclideanGeometry.angle (s.excenter signs) p (s.touchpoint signs i₂)
Affine.Simplex.angle_incenter_touchpoint_eq 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Affine.Simplex ℝ P n} {p : P} {i₁ i₂ : Fin (n + 1)} (hp₁ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points)) (hp₂ : p ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points)) : EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₁) = EuclideanGeometry.angle s.incenter p (s.touchpoint ∅ i₂)
Affine.Simplex.exists_excenterExists_and_eq_excenter_of_forall_angle_orthogonalProjectionSpan_eq 📋 Mathlib.Geometry.Euclidean.Angle.Incenter
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} [NeZero n] {s : Affine.Simplex ℝ P n} {p : P} (hp : p ∈ affineSpan ℝ (Set.range s.points)) {i₁ : Fin (n + 1)} (h : ∀ (i₂ : Fin (n + 1)), i₂ ≠ i₁ → ∃ p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₁).points), p' ∈ affineSpan ℝ (Set.range (s.faceOpposite i₂).points) ∧ EuclideanGeometry.angle p p' ↑((s.faceOpposite i₁).orthogonalProjectionSpan p) = EuclideanGeometry.angle p p' ↑((s.faceOpposite i₂).orthogonalProjectionSpan p)) : ∃ signs, s.ExcenterExists signs ∧ p = s.excenter signs
EuclideanGeometry.Sphere.angle_center_eq_zero_iff_eq 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hr : s.radius ≠ 0) : EuclideanGeometry.angle p₁ s.center p₂ = 0 ↔ p₁ = p₂
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ EuclideanGeometry.Sphere.ofDiameter p₁ p₃
EuclideanGeometry.Sphere.angle_center_eq_pi_iff_isDiameter 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hr : s.radius ≠ 0) : EuclideanGeometry.angle p₁ s.center p₂ = Real.pi ↔ s.IsDiameter p₁ p₂
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_of_isDiameter 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s
EuclideanGeometry.Sphere.thales_theorem 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} (hd : s.IsDiameter p₁ p₃) : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ s
EuclideanGeometry.Sphere.IsTangentAt_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} (h : EuclideanGeometry.angle q p s.center = Real.pi / 2) (hp : p ∈ s) : s.IsTangentAt p line[ℝ, p, q]
EuclideanGeometry.Sphere.IsTangentAt_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} (hp : p ∈ s) : s.IsTangentAt p line[ℝ, p, q] ↔ EuclideanGeometry.angle q p s.center = Real.pi / 2
EuclideanGeometry.Sphere.isDiameter_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} {s : EuclideanGeometry.Sphere P} [Fact (Module.finrank ℝ V = 2)] (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hne₁₂ : p₁ ≠ p₂) (hne₂₃ : p₂ ≠ p₃) (hangle : EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2) : s.IsDiameter p₁ p₃
EuclideanGeometry.Sphere.angle_center_eq_two_mul_angle_of_two_mul_angle_le_pi 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) (h : 2 * EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi) : EuclideanGeometry.angle p₁ s.center p₃ = 2 * EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} {as : AffineSubspace ℝ P} (h : s.IsTangentAt p as) (hq_mem : q ∈ as) : EuclideanGeometry.angle q p s.center = Real.pi / 2
EuclideanGeometry.Sphere.angle_center_eq_two_pi_sub_two_mul_angle_of_pi_le_two_mul_angle 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P} (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) (hp₃ : p₃ ∈ s) (hp₂p₁ : p₂ ≠ p₁) (hp₂p₃ : p₂ ≠ p₃) (h : Real.pi ≤ 2 * EuclideanGeometry.angle p₁ p₂ p₃) : EuclideanGeometry.angle p₁ s.center p₃ = 2 * Real.pi - 2 * EuclideanGeometry.angle p₁ p₂ p₃
Affine.Triangle.dist_div_sin_angle_eq_two_mul_circumradius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) = 2 * Affine.Simplex.circumradius t
Affine.Triangle.dist_div_sin_angle_div_two_eq_circumradius 📋 Mathlib.Geometry.Euclidean.Angle.Sphere
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : dist (t.points i₁) (t.points i₃) / Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃)) / 2 = Affine.Simplex.circumradius t
EuclideanGeometry.angle_eq_angle_of_dist_eq 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : dist p₁ p₂ = dist p₁ p₃) : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₃ p₂
EuclideanGeometry.angle_add_angle_add_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ : P} (p₃ : P) (h : p₂ ≠ p₁) : EuclideanGeometry.angle p₁ p₂ p₃ + EuclideanGeometry.angle p₂ p₃ p₁ + EuclideanGeometry.angle p₃ p₁ p₂ = Real.pi
EuclideanGeometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : EuclideanGeometry.angle p₁ p₂ p₃ = EuclideanGeometry.angle p₁ p₃ p₂) (hpi : EuclideanGeometry.angle p₂ p₁ p₃ ≠ Real.pi) : dist p₁ p₂ = dist p₁ p₃
EuclideanGeometry.law_sin 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) * dist p₃ p₁
EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) * dist p₃ p₁
EuclideanGeometry.sin_angle_div_dist_eq_sin_angle_div_dist 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h23 : p₂ ≠ p₃) (h31 : p₃ ≠ p₁) : Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) / dist p₃ p₁ = Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) / dist p₂ p₃
EuclideanGeometry.angle_add_angle_eq_of_sbtw 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a c p x : P} (hx : Sbtw ℝ a x c) : EuclideanGeometry.angle a p x + EuclideanGeometry.angle x p c = EuclideanGeometry.angle a p c
EuclideanGeometry.exterior_angle_eq_angle_add_angle 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (p : P) (h : Sbtw ℝ p p₁ p₂) : EuclideanGeometry.angle p₃ p₁ p = EuclideanGeometry.angle p₁ p₃ p₂ + EuclideanGeometry.angle p₃ p₂ p₁
EuclideanGeometry.angle_add_of_ne_of_ne 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p : P} (hb : a ≠ b) (hc : a ≠ c) (hp : Wbtw ℝ b p c) : EuclideanGeometry.angle b a p + EuclideanGeometry.angle p a c = EuclideanGeometry.angle b a c
EuclideanGeometry.pi_div_three_le_angle_of_le_of_le 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h₂₃₁ : EuclideanGeometry.angle p₂ p₃ p₁ ≤ EuclideanGeometry.angle p₁ p₂ p₃) (h₃₁₂ : EuclideanGeometry.angle p₃ p₁ p₂ ≤ EuclideanGeometry.angle p₁ p₂ p₃) : Real.pi / 3 ≤ EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.dist_lt_of_angle_lt 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} (h : ¬Collinear ℝ {a, b, c}) : EuclideanGeometry.angle a c b < EuclideanGeometry.angle a b c → dist a b < dist a c
EuclideanGeometry.angle_le_iff_dist_le 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} (h : ¬Collinear ℝ {a, b, c}) : EuclideanGeometry.angle a c b ≤ EuclideanGeometry.angle a b c ↔ dist a b ≤ dist a c
EuclideanGeometry.angle_lt_iff_dist_lt 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c : P} (h : ¬Collinear ℝ {a, b, c}) : EuclideanGeometry.angle a c b < EuclideanGeometry.angle a b c ↔ dist a b < dist a c
EuclideanGeometry.angle_le_pi_div_three_of_le_of_le 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h₂₃₁ : EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₂ p₃ p₁) (h₃₁₂ : EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₃ p₁ p₂) (hnd : p₁ ≠ p₂ ∨ p₁ ≠ p₃ ∨ p₂ ≠ p₃) : EuclideanGeometry.angle p₁ p₂ p₃ ≤ Real.pi / 3
EuclideanGeometry.dist_mul_of_eq_angle_of_dist_mul 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a b c a' b' c' : P) (r : ℝ) (h : EuclideanGeometry.angle a' b' c' = EuclideanGeometry.angle a b c) (hab : dist a' b' = r * dist a b) (hcb : dist c' b' = r * dist c b) : dist a' c' = r * dist a c
EuclideanGeometry.dist_eq_dist_mul_sin_angle_div_sin_angle 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h : ¬Collinear ℝ {p₁, p₂, p₃}) : dist p₁ p₂ = dist p₃ p₁ * Real.sin (EuclideanGeometry.angle p₂ p₃ p₁) / Real.sin (EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.angle_lt_pi_div_three_of_le_of_le_of_ne 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h₂₃₁ : EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₂ p₃ p₁) (h₃₁₂ : EuclideanGeometry.angle p₁ p₂ p₃ ≤ EuclideanGeometry.angle p₃ p₁ p₂) (hne : EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₂ p₃ p₁ ∨ EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₃ p₁ p₂ ∨ EuclideanGeometry.angle p₂ p₃ p₁ ≠ EuclideanGeometry.angle p₃ p₁ p₂) : EuclideanGeometry.angle p₁ p₂ p₃ < Real.pi / 3
EuclideanGeometry.pi_div_three_lt_angle_of_le_of_le_of_ne 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ : P} (h₂₃₁ : EuclideanGeometry.angle p₂ p₃ p₁ ≤ EuclideanGeometry.angle p₁ p₂ p₃) (h₃₁₂ : EuclideanGeometry.angle p₃ p₁ p₂ ≤ EuclideanGeometry.angle p₁ p₂ p₃) (hne : EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₂ p₃ p₁ ∨ EuclideanGeometry.angle p₁ p₂ p₃ ≠ EuclideanGeometry.angle p₃ p₁ p₂ ∨ EuclideanGeometry.angle p₂ p₃ p₁ ≠ EuclideanGeometry.angle p₃ p₁ p₂) : Real.pi / 3 < EuclideanGeometry.angle p₁ p₂ p₃
EuclideanGeometry.angle_add_angle_eq_of_sbtw_of_sameRay 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c p x : P} (hx : Sbtw ℝ a x c) (hxb : SameRay ℝ (x -ᵥ p) (b -ᵥ p)) (hb : b ≠ p) : EuclideanGeometry.angle a p b + EuclideanGeometry.angle b p c = EuclideanGeometry.angle a p c
EuclideanGeometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.law_cos 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ - 2 * dist p₁ p₂ * dist p₃ p₂ * Real.cos (EuclideanGeometry.angle p₁ p₂ p₃)
EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist 📋 Mathlib.Geometry.Euclidean.Triangle
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (a b c p : P) (h : EuclideanGeometry.angle b p c = Real.pi) : dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)
EuclideanGeometry.angle_le_angle_add_angle 📋 Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
{V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p p₁ p₂ p₃ : P) : EuclideanGeometry.angle p₁ p p₃ ≤ EuclideanGeometry.angle p₁ p p₂ + EuclideanGeometry.angle p₂ p p₃
EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_of_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.BritishFlag
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (ha : EuclideanGeometry.angle b a d = Real.pi / 2) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2
EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two 📋 Mathlib.Geometry.Euclidean.BritishFlag
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2 ↔ EuclideanGeometry.angle b a d = Real.pi / 2
EuclideanGeometry.dist_sq_add_dist_sq_eq_dist_sq_add_dist_sq_add_two_mul_dist_mul_dist_mul_cos_angle 📋 Mathlib.Geometry.Euclidean.BritishFlag
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {a b c d : P} (h : midpoint ℝ a c = midpoint ℝ b d) (p : P) : dist p a ^ 2 + dist p c ^ 2 = dist p b ^ 2 + dist p d ^ 2 + 2 * dist b a * dist d a * Real.cos (EuclideanGeometry.angle b a d)
EuclideanGeometry.angle_eq_of_congruent 📋 Mathlib.Geometry.Euclidean.Congruence
{ι : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {v₁ : ι → P₁} {v₂ : ι → P₂} (h : Congruent v₁ v₂) (i j k : ι) : EuclideanGeometry.angle (v₁ i) (v₁ j) (v₁ k) = EuclideanGeometry.angle (v₂ i) (v₂ j) (v₂ k)
EuclideanGeometry.side_angle_side 📋 Mathlib.Geometry.Euclidean.Congruence
{V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c') (hd₁ : dist a b = dist a' b') (hd₂ : dist b c = dist b' c') : Congruent ![a, b, c] ![a', b', c']
EuclideanGeometry.angle_angle_side 📋 Mathlib.Geometry.Euclidean.Congruence
{V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : ¬Collinear ℝ {a, b, c}) (ha₁ : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c') (ha₂ : EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a') (hd : dist c a = dist c' a') : Congruent ![a, b, c] ![a', b', c']
EuclideanGeometry.angle_side_angle 📋 Mathlib.Geometry.Euclidean.Congruence
{V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : ¬Collinear ℝ {a, b, c}) (ha₁ : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c') (hd : dist b c = dist b' c') (ha₂ : EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a') : Congruent ![a, b, c] ![a', b', c']
Similar.angle_eq 📋 Mathlib.Geometry.Euclidean.Similarity
{V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : Similar ![a, b, c] ![a', b', c']) : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c'
Similar.angle_eq_all 📋 Mathlib.Geometry.Euclidean.Similarity
{V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h : Similar ![a, b, c] ![a', b', c']) : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' ∧ EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' ∧ EuclideanGeometry.angle c a b = EuclideanGeometry.angle c' a' b'
EuclideanGeometry.similar_of_angle_angle 📋 Mathlib.Geometry.Euclidean.Similarity
{V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h_not_col : ¬Collinear ℝ {a, b, c}) (h₁ : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c') (h₂ : EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a') : Similar ![a, b, c] ![a', b', c']
EuclideanGeometry.similar_of_side_angle_side 📋 Mathlib.Geometry.Euclidean.Similarity
{V₁ : Type u_1} {V₂ : Type u_2} {P₁ : Type u_3} {P₂ : Type u_4} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₁] [InnerProductSpace ℝ V₂] [MetricSpace P₁] [MetricSpace P₂] [NormedAddTorsor V₁ P₁] [NormedAddTorsor V₂ P₂] {a b c : P₁} {a' b' c' : P₂} (h_not_col : ¬Collinear ℝ {a, b, c}) (h_not_col' : ¬Collinear ℝ {a', b', c'}) (h : EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c') (hd : dist a b * dist b' c' = dist b c * dist a' b') : Similar ![a, b, c] ![a', b', c']
Affine.Simplex.Equilateral.angle_eq_pi_div_three 📋 Mathlib.Geometry.Euclidean.Simplex
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P n} (he : s.Equilateral) {i₁ i₂ i₃ : Fin (n + 1)} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : EuclideanGeometry.angle (s.points i₁) (s.points i₂) (s.points i₃) = Real.pi / 3
Affine.Triangle.acuteAngled_iff_angle_lt 📋 Mathlib.Geometry.Euclidean.Simplex
{V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {t : Affine.Triangle ℝ P} : Affine.Simplex.AcuteAngled t ↔ EuclideanGeometry.angle (t.points 0) (t.points 1) (t.points 2) < Real.pi / 2 ∧ EuclideanGeometry.angle (t.points 1) (t.points 2) (t.points 0) < Real.pi / 2 ∧ EuclideanGeometry.angle (t.points 2) (t.points 0) (t.points 1) < Real.pi / 2
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Sphere.Power
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapb : EuclideanGeometry.angle a p b = Real.pi) (hcpd : EuclideanGeometry.angle c p d = Real.pi) : dist a p * dist b p = dist c p * dist d p
EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_zero 📋 Mathlib.Geometry.Euclidean.Sphere.Power
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hab : a ≠ b) (hcd : c ≠ d) (hapb : EuclideanGeometry.angle a p b = 0) (hcpd : EuclideanGeometry.angle c p d = 0) : dist a p * dist b p = dist c p * dist d p
EuclideanGeometry.cospherical_of_mul_dist_eq_mul_dist_of_angle_eq_pi 📋 Mathlib.Geometry.Euclidean.Sphere.Power
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {p₁ p₂ p₃ p₄ p : P} (h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p) (hp₁p₂ : EuclideanGeometry.angle p₁ p p₂ = Real.pi) (hp₃p₄ : EuclideanGeometry.angle p₃ p p₄ = Real.pi) (hn : ¬Collinear ℝ {p₁, p, p₃}) : EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
EuclideanGeometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical 📋 Mathlib.Geometry.Euclidean.Sphere.Ptolemy
{V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {P : Type u_2} [MetricSpace P] [NormedAddTorsor V P] {a b c d p : P} (h : EuclideanGeometry.Cospherical {a, b, c, d}) (hapc : EuclideanGeometry.angle a p c = Real.pi) (hbpd : EuclideanGeometry.angle b p d = Real.pi) : dist a b * dist c d + dist b c * dist d a = dist a c * dist b d

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59