1. FormalConjecturesForMathlib
  2. Geometry
  3. «2d»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.LinearAlgebra.Orientation public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine public import Mathlib.Geometry.Euclidean.Triangle public import Mathlib.Data.Set.Card public import Mathlib.Geometry.Euclidean.Sphere.Basic public import FormalConjecturesForMathlib.Geometry.Metric public import FormalConjecturesForMathlib.Logic.Equiv.Fin.Rotate public import FormalConjecturesForMathlib.Data.Set.Triplewise@[expose] public sectionscoped[EuclideanGeometry] notation "ℝ²" => EuclideanSpace ℝ (Fin 2)open scoped EuclideanGeometry Finset

Oriented angles make sense in 2d.

Note: this can't blindly be added to mathlib as it creates an "instance diamond" with an instance for modules satisfying is_empty.

noncomputable instance Module.orientedEuclideanSpaceFinTwo : Module.Oriented ℝ ℝ² (Fin 2) := ⟨Basis.orientation <| PiLp.basisFun 2 _ _⟩

Two dimensional euclidean space is two-dimensional.

instance fact_finrank_euclideanSpace_fin_two : Fact (Module.finrank ℝ ℝ² = 2) := ⟨finrank_euclideanSpace_fin⟩open scoped EuclideanGeometryopen scoped Realnamespace EuclideanGeometryvariable {V P : Type*} {n : ℕ}variable [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]variable [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin n → P}

We say a subset A of points in the plane is non-trilinear if it contains no three points that lie on the same line.

def NonTrilinear (A : Set P) : Prop := A.Triplewise (fun x y z ↦ ¬ Collinear ℝ {x, y, z})

We say a subset S of points is non-collinear for $n$ points if it contains no $n$ points that lie on the same line.

def NonCollinearFor (n : ℕ) (S : Set P) : Prop := ∀ (A : Set P), A ⊆ S → A.Finite → A.ncard = n → ¬ Collinear ℝ Aomit [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] in lemma NonCollinearFor.subset {n : ℕ} {S T : Set P} (h : S ⊆ T) (hS : NonCollinearFor n T) : NonCollinearFor n S := V:Type u_1P:Type u_2inst✝³:NormedAddCommGroup Vinst✝²:InnerProductSpace ℝ Vinst✝¹:MetricSpace Pinst✝:NormedAddTorsor V Pn:ℕS:Set PT:Set Ph:S ⊆ ThS:NonCollinearFor n T⊢ NonCollinearFor n S V:Type u_1P:Type u_2inst✝³:NormedAddCommGroup Vinst✝²:InnerProductSpace ℝ Vinst✝¹:MetricSpace Pinst✝:NormedAddTorsor V Pn:ℕS:Set PT:Set Ph:S ⊆ ThS:NonCollinearFor n TA:Set PhA:A ⊆ ShFin:A.FinitehCard:A.ncard = n⊢ ¬Collinear ℝ A All goals completed! 🐙

ConvexIndep S means that S consists of extremal points of its convex hull, i.e., the point set encloses a convex shape. Also known as a "convex-independent set".

def ConvexIndep (S : Set ℝ²) : Prop := ∀ a ∈ S, a ∉ convexHull ℝ (S \ {a})

The set P contains a convex n-gon. See also IsConvexPolygon.

def HasConvexNGon (n : ℕ) (P : Set ℝ²) : Prop := ∃ S : Finset ℝ², S.card = n ∧ ↑S ⊆ P ∧ ConvexIndep S

The statement that a sequence of points form a counter-clockwise convex polygon.

def IsCcwConvexPolygon (p : Fin n → P) : Prop := ∀ ⦃i j k⦄, i < j → j < k → (∡ (p i) (p j) (p k)).sign = 1theorem IsCcwConvexPolygon.sign_oangle (hp : IsCcwConvexPolygon p) {i j k : Fin n} (hij : i < j) (hjk : j < k) : (∡ (p i) (p j) (p k)).sign = 1 := hp hij hjkV:Type u_1P:Type u_2n:ℕinst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin n → Php:IsCcwConvexPolygon pi:Fin nj:Fin nk:Fin nhij:i < jhjk:j < k⊢ (∡ (p i) (p j) (p k)).sign = 1 All goals completed! 🐙V:Type u_1P:Type u_2n:ℕinst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin n → Php:IsCcwConvexPolygon pi:Fin nj:Fin nk:Fin nhij:i < jhjk:j < k⊢ (∡ (p i) (p j) (p k)).sign = 1 All goals completed! 🐙V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3hi:¬0 = Fin.last (n + 2)hi':1 = Fin.last (n + 2)⊢ False All goals completed! 🐙 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ i < (finRotate (n + 3)) iV:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ (finRotate (n + 3)) i < (finRotate (n + 3)) ((finRotate (n + 3)) i) V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ i < (finRotate (n + 3)) iV:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ (finRotate (n + 3)) i < (finRotate (n + 3)) ((finRotate (n + 3)) i) V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ (finRotate (n + 3)) i ≠ Fin.last (n + 2) V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ i ≠ Fin.last (n + 2)V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)n:ℕp:Fin (n + 3) → Php:IsCcwConvexPolygon phn:3 ≤ n + 3i:Fin (n + 3)hi:¬i = Fin.last (n + 2)hi':¬(finRotate (n + 3)) i = Fin.last (n + 2)⊢ (finRotate (n + 3)) i ≠ Fin.last (n + 2) All goals completed! 🐙@[simp] theorem isCcwConvexPolygon_zero (p : Fin 0 → P) : IsCcwConvexPolygon p := finZeroElim@[simp] theorem isCcwConvexPolygon_one (p : Fin 1 → P) : IsCcwConvexPolygon p := V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 1 → P⊢ IsCcwConvexPolygon p V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 1 → Pi✝:Fin 1⊢ ∀ ⦃j k : Fin 1⦄, i✝ < j → j < k → (∡ (p i✝) (p j) (p k)).sign = 1; All goals completed! 🐙@[simp] theorem isCcwConvexPolygon_two (p : Fin 2 → P) : IsCcwConvexPolygon p := V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 2 → P⊢ IsCcwConvexPolygon p V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 2 → Pi✝:Fin 2⊢ ∀ ⦃j k : Fin 2⦄, i✝ < j → j < k → (∡ (p i✝) (p j) (p k)).sign = 1; All goals completed! 🐙V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 4 → Px✝:(∡ (p 0) (p 1) (p 2)).sign = 1 ∧ (∡ (p 1) (p 2) (p 3)).sign = 1 ∧ (∡ (p 2) (p 3) (p 0)).sign = 1 ∧ (∡ (p 3) (p 0) (p 1)).sign = 1h1:(∡ (p 0) (p 1) (p 2)).sign = 1h2:(∡ (p 1) (p 2) (p 3)).sign = 1h3:(∡ (p 2) (p 3) (p 0)).sign = 1h4:(∡ (p 3) (p 0) (p 1)).sign = 1hij:Truehjk:True⊢ (∡ (p ((fun i ↦ i) ⟨2, ⋯⟩)) (p ((fun i ↦ i) ⟨3, ⋯⟩)) (p ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1 All goals completed! 🐙 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)p:Fin 4 → Px✝:(∡ (p 0) (p 1) (p 2)).sign = 1 ∧ (∡ (p 1) (p 2) (p 3)).sign = 1 ∧ (∡ (p 2) (p 3) (p 0)).sign = 1 ∧ (∡ (p 3) (p 0) (p 1)).sign = 1h1:(∡ (p 0) (p 1) (p 2)).sign = 1h2:(∡ (p 1) (p 2) (p 3)).sign = 1h3:(∡ (p 2) (p 3) (p 0)).sign = 1h4:(∡ (p 3) (p 0) (p 1)).sign = 1hij:Truehjk:True⊢ (∡ (p ((fun i ↦ i) ⟨1, ⋯⟩)) (p ((fun i ↦ i) ⟨2, ⋯⟩)) (p ((fun i ↦ i) ⟨3, ⋯⟩))).sign = 1 All goals completed! 🐙@[simp] theorem isCcwConvexPolygon_four (A B C D : P) : IsCcwConvexPolygon ![A, B, C, D] ↔ (∡ A B C).sign = 1 ∧ (∡ B C D).sign = 1 ∧ (∡ C D A).sign = 1 ∧ (∡ D A B).sign = 1 := isCcwConvexPolygon_four'

The statement that a sequence of points form a convex polygon.

def IsConvexPolygon {n : ℕ} (p : Fin n → P) : Prop := IsCcwConvexPolygon p ∨ IsCcwConvexPolygon fun i => p (-i)

Three affine independent points always form a convex polygon.

V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.neghij:Truehjk:True⊢ (∡ ((fun i ↦ ![A, B, C] (-i)) ((fun i ↦ i) ⟨2, ⋯⟩)) ((fun i ↦ ![A, B, C] (-i)) ((fun i ↦ i) ⟨1, ⋯⟩)) ((fun i ↦ ![A, B, C] (-i)) ((fun i ↦ i) ⟨0, ⋯⟩))).sign = -1 All goals completed! 🐙 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.pos⊢ IsConvexPolygon ![A, B, C] V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.pos⊢ IsCcwConvexPolygon ![A, B, C] V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posi:Fin (Nat.succ 0).succ.succj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhij:i < jhjk:j < k⊢ (∡ (![A, B, C] i) (![A, B, C] j) (![A, B, C] k)).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨0, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨1, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨2, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨0, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨1, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posj:Fin (Nat.succ 0).succ.succk:Fin (Nat.succ 0).succ.succhjk:j < khij:(fun i ↦ i) ⟨2, ⋯⟩ < j⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] j) (![A, B, C] k)).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨0, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨1, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨2, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] k)).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨0, ⋯⟩ < khij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨1, ⋯⟩ < khij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨2, ⋯⟩ < khij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨0, ⋯⟩ < khij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨1, ⋯⟩ < khij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨2, ⋯⟩ < khij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨0, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨1, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] k)).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.posk:Fin (Nat.succ 0).succ.succhjk:(fun i ↦ i) ⟨2, ⋯⟩ < khij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] k)).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1 V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩hjk:(fun i ↦ i) ⟨0, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩hjk:(fun i ↦ i) ⟨1, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨0, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨0, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨1, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨1, ⋯⟩))).sign = 1V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:PhABC:(∡ A B C).sign ≠ 0hsABC:(∡ A B C).sign = SignType.poshij:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩hjk:(fun i ↦ i) ⟨2, ⋯⟩ < (fun i ↦ i) ⟨2, ⋯⟩⊢ (∡ (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩)) (![A, B, C] ((fun i ↦ i) ⟨2, ⋯⟩))).sign = 1 All goals completed! 🐙 All goals completed! 🐙V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:Pp:Fin (Nat.succ 0).succ.succ → P := ![A, B, C]h:IsCcwConvexPolygon fun i ↦ p (-i)⊢ (∡ (p 0) (p 2) (p 1)).sign = 1 exact h.sign_oangle (i := 0) (j := 1) (k := 2) (V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:Pp:Fin (Nat.succ 0).succ.succ → P := ![A, B, C]h:IsCcwConvexPolygon fun i ↦ p (-i)⊢ 0 < 1 All goals completed! 🐙) (V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)A:PB:PC:Pp:Fin (Nat.succ 0).succ.succ → P := ![A, B, C]h:IsCcwConvexPolygon fun i ↦ p (-i)⊢ 1 < 2 All goals completed! 🐙)V:Type u_1P:Type u_2inst✝⁵:NormedAddCommGroup Vinst✝⁴:InnerProductSpace ℝ Vinst✝³:MetricSpace Pinst✝²:NormedAddTorsor V Pinst✝¹:Module.Oriented ℝ V (Fin 2)inst✝:Fact (Module.finrank ℝ V = 2)t:Affine.Triangle ℝ Pthis:t.points = ![t.points 0, t.points 1, t.points 2]⊢ AffineIndependent ℝ t.points All goals completed! 🐙noncomputable def triangle_area (a b c : P) : ℝ := positiveOrientation.areaForm (a -ᵥ c) (b -ᵥ c) / 2a:ℝ²b:ℝ²c:ℝ²⊢ (a.ofLp 0 - c.ofLp 0) * (b.ofLp 1 - c.ofLp 1) - (b.ofLp 0 - c.ofLp 0) * (a.ofLp 1 - c.ofLp 1) = a.ofLp 0 * b.ofLp 1 - a.ofLp 0 * c.ofLp 1 - b.ofLp 0 * a.ofLp 1 + b.ofLp 0 * c.ofLp 1 + c.ofLp 0 * a.ofLp 1 - c.ofLp 0 * b.ofLp 1 All goals completed! 🐙

The minimum number of distinct distances guaranteed for any set of $n$ points.

noncomputable def minimalDistinctDistances (n : ℕ) : ℕ := sInf {(distinctDistances points : ℝ) | (points : Finset ℝ²) (_ : points.card = n)}

Let $x_1,\ldots,x_n\in \mathbb{R}^2$ and let $R(x_i)=#{ \lvert x_j-x_i\rvert : j\neq i}$, where the points are ordered such that $$R(x_1)\leq \cdots \leq R(x_n).$$ Let $g(n)$ be the maximum number of distinct values the $R(x_i)$ can take.

noncomputable def maximalDistinctDistancesFrom (n : ℕ) : ℕ := sSup {#(X.image (distinctDistancesFrom X)) | (X : Finset ℝ²) (_ : #X = n)}

A collection $x_1, \dots, x_n\in\mathbb{R}^2$ is in general position if no three are collinear and no four lie on a circle.

Stated for Set ℝ² so that infinite collections are covered; a Finset argument coerces.

def InGeneralPosition (X : Set ℝ²) : Prop := NonTrilinear X ∧ ∀ T ⊆ X, T.ncard = 4 → ¬Cospherical T

a b c are the vertices of a right-angled triangle: the (unoriented) angle at one of the three vertices equals π / 2.

def IsRightAngled (a b c : P) : Prop := ∠ b a c = π / 2 ∨ ∠ a b c = π / 2 ∨ ∠ b c a = π / 2

a b c d are the vertices, in counter-clockwise order, of an isosceles trapezoid: they are in strictly convex position, the side ab is parallel to the side cd (the two bases), and the diagonals ac and bd have equal length. One pair of parallel sides together with equal diagonals is the classical characterization of an isosceles trapezoid; in particular it rules out non-rectangular parallelograms.

def IsIsoscelesTrapezoid (a b c d : ℝ²) : Prop := IsCcwConvexPolygon ![a, b, c, d] ∧ (affineSpan ℝ {a, b}).Parallel (affineSpan ℝ {c, d}) ∧ dist a c = dist b dend EuclideanGeometrydef IsIsosceles {α : Type*} [Dist α] (p q r : α) : Prop := dist p q = dist q r ∨ dist q r = dist r p ∨ dist r p = dist p qnonrec def Set.IsIsosceles {α : Type} [Dist α] (A : Set α) := Nonempty A ∧ A.Triplewise (IsIsosceles · · ·)