def EuclideanGeometry.«termℝ²» : Lean.ParserDescr

Equations

• EuclideanGeometry.«termℝ²» = Lean.ParserDescr.node `EuclideanGeometry.«termℝ²» 1024 (Lean.ParserDescr.symbol "ℝ²")

noncomputable instance Module.orientedEuclideanSpaceFinTwo : Oriented ℝ (EuclideanSpace ℝ (Fin 2)) (Fin 2)

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.

Equations

• Module.orientedEuclideanSpaceFinTwo = { positiveOrientation := (Pi.basisFun ℝ (Fin 2)).orientation }

instance fact_finrank_euclideanSpace_fin_two : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2)

Two dimensional euclidean space is two-dimensional.

def EuclideanGeometry.IsCcwConvexPolygon {V : Type u_1} {P : Type u_2} {n : ℕ} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (p : Fin n → P) : Prop

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

Equations

• EuclideanGeometry.IsCcwConvexPolygon p = ∀ ⦃i j k : Fin n⦄, i < j → j < k → (EuclideanGeometry.oangle (p i) (p j) (p k)).sign = 1

theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle {V : Type u_1} {P : Type u_2} {n : ℕ} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin n → P} (hp : IsCcwConvexPolygon p) {i j k : Fin n} (hij : i < j) (hjk : j < k) : (oangle (p i) (p j) (p k)).sign = 1

theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle' {V : Type u_1} {P : Type u_2} {n : ℕ} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin n → P} (hp : IsCcwConvexPolygon p) {i j k : Fin n} (hij : i < j) (hjk : j < k) : (oangle (p j) (p k) (p i)).sign = 1

theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle'' {V : Type u_1} {P : Type u_2} {n : ℕ} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin n → P} (hp : IsCcwConvexPolygon p) {i j k : Fin n} (hij : i < j) (hjk : j < k) : (oangle (p k) (p i) (p j)).sign = 1

theorem EuclideanGeometry.IsCcwConvexPolygon.sign_oangle_finRotate {V : Type u_1} {P : Type u_2} {n : ℕ} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin n → P} (hp : IsCcwConvexPolygon p) (hn : 3 ≤ n) (i : Fin n) : (oangle (p i) (p ((finRotate n) i)) (p ((finRotate n) ((finRotate n) i)))).sign = 1

@[simp]

theorem EuclideanGeometry.isCcwConvexPolygon_zero {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (p : Fin 0 → P) : IsCcwConvexPolygon p

@[simp]

theorem EuclideanGeometry.isCcwConvexPolygon_one {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (p : Fin 1 → P) : IsCcwConvexPolygon p

@[simp]

theorem EuclideanGeometry.isCcwConvexPolygon_two {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (p : Fin 2 → P) : IsCcwConvexPolygon p

theorem EuclideanGeometry.isCcwConvexPolygon_four' {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {p : Fin 4 → P} : IsCcwConvexPolygon p ↔ (oangle (p 0) (p 1) (p 2)).sign = 1 ∧ (oangle (p 1) (p 2) (p 3)).sign = 1 ∧ (oangle (p 2) (p 3) (p 0)).sign = 1 ∧ (oangle (p 3) (p 0) (p 1)).sign = 1

@[simp]

theorem EuclideanGeometry.isCcwConvexPolygon_four {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (A B C D : P) : IsCcwConvexPolygon ![A, B, C, D] ↔ (oangle A B C).sign = 1 ∧ (oangle B C D).sign = 1 ∧ (oangle C D A).sign = 1 ∧ (oangle D A B).sign = 1

def EuclideanGeometry.IsConvexPolygon {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {n : ℕ} (p : Fin n → P) : Prop

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

Equations

• EuclideanGeometry.IsConvexPolygon p = (EuclideanGeometry.IsCcwConvexPolygon p ∨ EuclideanGeometry.IsCcwConvexPolygon fun (i : Fin n) => p (-i))

theorem EuclideanGeometry.isConvexPolygon_three_of_affineIndependent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {A B C : P} (hABC : AffineIndependent ℝ ![A, B, C]) : IsConvexPolygon ![A, B, C]

Three affine independent points always form a convex polygon.

theorem EuclideanGeometry.isConvexPolygon_three_iff_affineIndependent {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] {A B C : P} : IsConvexPolygon ![A, B, C] ↔ AffineIndependent ℝ ![A, B, C]

theorem EuclideanGeometry.isConvexPolygon_triangle {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (t : Affine.Triangle ℝ P) : IsConvexPolygon t.points

noncomputable def EuclideanGeometry.triangle_area {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Module.Oriented ℝ V (Fin 2)] [Fact (Module.finrank ℝ V = 2)] (a b c : P) : ℝ

Equations

• EuclideanGeometry.triangle_area a b c = (positiveOrientation.areaForm (a -ᵥ c)) (b -ᵥ c) / 2

theorem EuclideanGeometry.triangle_area_eq_det (a b c : EuclideanSpace ℝ (Fin 2)) : triangle_area a b c = !![a 0, b 0, c 0; a 1, b 1, c 1; 1, 1, 1].det / 2

def IsIsosceles {α : Type u_1} [Dist α] (p q r : α) : Prop

Equations

• IsIsosceles p q r = (dist p q = dist q r ∨ dist q r = dist r p ∨ dist r p = dist p q)