LeanPool.Monsky.BasicDefinitions

Imported Lean Pool material for LeanPool.Monsky.BasicDefinitions.

def LeanPool.Monsky.isCover {n : ℕ} (X : Set (EuclideanSpace ℝ (Fin 2))) (S : Set (Fin n → EuclideanSpace ℝ (Fin 2))) : Prop

X equals the union of the closed hulls of the polygons in S.

Equations

• LeanPool.Monsky.isCover X S = (X = ⋃ P ∈ S, LeanPool.Monsky.closedHull P)

def LeanPool.Monsky.isDisjointPolygonSet {n : ℕ} (S : Set (Fin n → EuclideanSpace ℝ (Fin 2))) : Prop

The open hulls of distinct polygons in S are pairwise disjoint.

Equations

• LeanPool.Monsky.isDisjointPolygonSet S = ∀ T₁ ∈ S, ∀ T₂ ∈ S, T₁ ≠ T₂ → Disjoint (LeanPool.Monsky.openHull T₁) (LeanPool.Monsky.openHull T₂)

def LeanPool.Monsky.isDisjointCover {n : ℕ} (X : Set (EuclideanSpace ℝ (Fin 2))) (S : Set (Fin n → EuclideanSpace ℝ (Fin 2))) : Prop

isDisjointCover X S states that S covers X and its open hulls are pairwise disjoint.

Equations

• LeanPool.Monsky.isDisjointCover X S = (LeanPool.Monsky.isCover X S ∧ LeanPool.Monsky.isDisjointPolygonSet S)

noncomputable def LeanPool.Monsky.triangleArea (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : ℝ

The area of a triangle, given by half the absolute value of its determinant.

Equations

• LeanPool.Monsky.triangleArea T = |LeanPool.Monsky.det T| / 2

def LeanPool.Monsky.isEqualAreaCover (X : Set (EuclideanSpace ℝ (Fin 2))) (S : Set (Fin 3 → EuclideanSpace ℝ (Fin 2))) : Prop

A disjoint cover of X by triangles all having the same area.

Equations

• LeanPool.Monsky.isEqualAreaCover X S = (LeanPool.Monsky.isDisjointCover X S ∧ ∃ (area : ℝ), ∀ T ∈ S, LeanPool.Monsky.triangleArea T = area)

theorem LeanPool.Monsky.isCover_sub {n : ℕ} {S : Set (Fin n → EuclideanSpace ℝ (Fin 2))} {X : Set (EuclideanSpace ℝ (Fin 2))} (hCover : isCover X S) (Δ : Fin n → EuclideanSpace ℝ (Fin 2)) : Δ ∈ S → closedHull Δ ⊆ X

theorem LeanPool.Monsky.isCover_includes {n : ℕ} {S : Set (Fin n → EuclideanSpace ℝ (Fin 2))} {X : Set (EuclideanSpace ℝ (Fin 2))} {x : EuclideanSpace ℝ (Fin 2)} (hCover : isCover X S) (hx : x ∈ X) : ∃ P ∈ S, x ∈ closedHull P

theorem LeanPool.Monsky.isCover_open_el_imp_eq {n : ℕ} {S : Set (Fin n → EuclideanSpace ℝ (Fin 2))} (hDisj : isDisjointPolygonSet S) {Δ₁ Δ₂ : Fin n → EuclideanSpace ℝ (Fin 2)} (hΔ₁ : Δ₁ ∈ S) (hΔ₂ : Δ₂ ∈ S) {x : EuclideanSpace ℝ (Fin 2)} (hx₁ : x ∈ openHull Δ₁) (hx₂ : x ∈ openHull Δ₂) : Δ₁ = Δ₂

theorem LeanPool.Monsky.cover_mem_side {S : Set (Fin 3 → EuclideanSpace ℝ (Fin 2))} {X : Set (EuclideanSpace ℝ (Fin 2))} (hCover : isDisjointCover X S) (hArea : ∀ Δ ∈ S, det Δ ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ X) (hInt : ∀ Δ ∈ S, x ∉ openHull Δ) (hv : ∀ (i : Fin 3), ∀ Δ ∈ S, x ≠ Δ i) : ∃ Δ ∈ S, ∃ (i : Fin 3), x ∈ openHull (Tside Δ i)

theorem LeanPool.Monsky.no_empty_cover {n : ℕ} {S : Finset (Fin n → EuclideanSpace ℝ (Fin 2))} {X : Set (EuclideanSpace ℝ (Fin 2))} (hCover : isCover X ↑S) (hX : X.Nonempty) : S.card > 0