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 := (PiLp.basisFun 2 ℝ (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.NonTrilinear {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (A : Set P) : Prop

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.

Equations

• EuclideanGeometry.NonTrilinear A = A.Triplewise fun (x y z : P) => ¬Collinear ℝ {x, y, z}

def EuclideanGeometry.NonCollinearFor {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (n : ℕ) (S : Set P) : Prop

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.

Equations

• EuclideanGeometry.NonCollinearFor n S = ∀ A ⊆ S, A.Finite → A.ncard = n → ¬Collinear ℝ A

theorem EuclideanGeometry.NonCollinearFor.subset {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} {S T : Set P} (h : S ⊆ T) (hS : NonCollinearFor n T) : NonCollinearFor n S

def EuclideanGeometry.ConvexIndep (S : Set (EuclideanSpace ℝ (Fin 2))) : Prop

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".

Equations

• EuclideanGeometry.ConvexIndep S = ∀ a ∈ S, a ∉ (convexHull ℝ) (S \ {a})

def EuclideanGeometry.HasConvexNGon (n : ℕ) (P : Set (EuclideanSpace ℝ (Fin 2))) : Prop

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

Equations

• EuclideanGeometry.HasConvexNGon n P = ∃ (S : Finset (EuclideanSpace ℝ (Fin 2))), S.card = n ∧ ↑S ⊆ P ∧ EuclideanGeometry.ConvexIndep ↑S

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.ofLp 0, b.ofLp 0, c.ofLp 0; a.ofLp 1, b.ofLp 1, c.ofLp 1; 1, 1, 1].det / 2

noncomputable def EuclideanGeometry.distinctDistances (points : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

Given a finite set of points in the plane, we define the number of distinct distances between pairs of points.

Equations

• EuclideanGeometry.distinctDistances points = (Finset.image (fun (pair : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)) => dist pair.1 pair.2) points.offDiag).card

noncomputable def EuclideanGeometry.minimalDistinctDistances (n : ℕ) : ℕ

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EuclideanGeometry.distinctDistancesFrom (points : Finset (EuclideanSpace ℝ (Fin 2))) (pt : EuclideanSpace ℝ (Fin 2)) : ℕ

Given a finite set of points in the, we define the number of distinct distances between a given point and all other points

Equations

• EuclideanGeometry.distinctDistancesFrom points pt = (Finset.image (fun (x : EuclideanSpace ℝ (Fin 2)) => dist x pt) points).card

noncomputable def EuclideanGeometry.maximalDistinctDistancesFrom (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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def EuclideanGeometry.unitDistancePairsCount (points : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

Given a finite set of points, this function counts the number of unordered pairs of distinct points that are at a distance of exactly $1$ from each other.

Equations

• EuclideanGeometry.unitDistancePairsCount points = {p ∈ points.offDiag | dist p.1 p.2 = 1}.card / 2

def EuclideanGeometry.InGeneralPosition (X : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

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.

Equations

• EuclideanGeometry.InGeneralPosition X = (EuclideanGeometry.NonTrilinear ↑X ∧ ∀ T ⊆ X, T.card = 4 → ¬EuclideanGeometry.Cospherical ↑T)

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)

def Set.IsIsosceles {α : Type} [Dist α] (A : Set α) : Prop

Equations

• A.IsIsosceles = (Nonempty ↑A ∧ A.Triplewise fun (x1 x2 x3 : α) => IsIsosceles x1 x2 x3)