LeanPool.Monsky.MonskyEven

Imported Lean Pool material for LeanPool.Monsky.MonskyEven.

def LeanPool.Monsky.disjointSet {α β : Type} (X : Set α) (f : α → Set β) : Prop

disjointSet X f states that f sends distinct elements of X to disjoint sets.

Equations

• LeanPool.Monsky.disjointSet X f = ∀ (a₁ a₂ : α), a₁ ∈ X → a₂ ∈ X → a₁ ≠ a₂ → Disjoint (f a₁) (f a₂)

def LeanPool.Monsky.covers {α : Type u_1} {β : Type u_2} (X : Set α) (Y : Set β) (f : α → Set β) : Prop

covers X Y f states that Y is the union of f a over a ∈ X.

Equations

• LeanPool.Monsky.covers X Y f = (Y = ⋃ a ∈ X, f a)

theorem LeanPool.Monsky.isCover_iff (X : Set (EuclideanSpace ℝ (Fin 2))) (S : Set (Fin 3 → EuclideanSpace ℝ (Fin 2))) : isDisjointCover X S ↔ covers S X closedHull ∧ disjointSet S openHull

theorem LeanPool.Monsky.disjoint_aux {α β : Type} (S₁ S₂ : Set α) (f : α → Set β) (h₁ : disjointSet S₁ f) (h₂ : disjointSet S₂ f) (h₃ : ∀ (a₁ a₂ : α), a₁ ∈ S₁ → a₂ ∈ S₂ → Disjoint (f a₁) (f a₂)) : disjointSet (S₁ ∪ S₂) f

def LeanPool.Monsky.Δ₀ : Fin 3 → EuclideanSpace ℝ (Fin 2)

The lower triangle of the standard two-triangle dissection of the unit square.

Equations

• LeanPool.Monsky.Δ₀ 0 = LeanPool.Monsky.v 0 0
• LeanPool.Monsky.Δ₀ 1 = LeanPool.Monsky.v 1 0
• LeanPool.Monsky.Δ₀ 2 = LeanPool.Monsky.v 0 1

def LeanPool.Monsky.Δ₀' : Fin 3 → EuclideanSpace ℝ (Fin 2)

The upper triangle of the standard two-triangle dissection of the unit square.

Equations

• LeanPool.Monsky.Δ₀' 0 = LeanPool.Monsky.v 1 0
• LeanPool.Monsky.Δ₀' 1 = LeanPool.Monsky.v 0 1
• LeanPool.Monsky.Δ₀' 2 = LeanPool.Monsky.v 1 1

theorem LeanPool.Monsky.areaΔ₀ : triangleArea Δ₀ = 1 / 2

theorem LeanPool.Monsky.areaΔ₀' : triangleArea Δ₀' = 1 / 2

def LeanPool.Monsky.scaleVector (a : ℝ) (y : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

Scales the second coordinate of a plane vector by a.

Equations

• LeanPool.Monsky.scaleVector a y = !₂[y.ofLp 0, a * y.ofLp 1]

def LeanPool.Monsky.scaleTriangle (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Fin 3 → EuclideanSpace ℝ (Fin 2)

Applies scaleVector a to every vertex of a triangle.

Equations

• LeanPool.Monsky.scaleTriangle a T i = LeanPool.Monsky.scaleVector a (T i)

theorem LeanPool.Monsky.scaleTriangle_det (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : det (scaleTriangle a T) = a * det T

theorem LeanPool.Monsky.scaleTriangle_area (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : triangleArea (scaleTriangle a T) = |a| * triangleArea T

def LeanPool.Monsky.translateVector (a : ℝ) (x : EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

Translates the second coordinate of a plane vector by a.

Equations

• LeanPool.Monsky.translateVector a x = !₂[x.ofLp 0, a + x.ofLp 1]

def LeanPool.Monsky.translateTriangle (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : Fin 3 → EuclideanSpace ℝ (Fin 2)

Applies translateVector a to every vertex of a triangle.

Equations

• LeanPool.Monsky.translateTriangle a T i = LeanPool.Monsky.translateVector a (T i)

theorem LeanPool.Monsky.translateTriangle_det (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : det (translateTriangle a T) = det T

theorem LeanPool.Monsky.translateTriangle_area (a : ℝ) (T : Fin 3 → EuclideanSpace ℝ (Fin 2)) : triangleArea (translateTriangle a T) = triangleArea T

theorem LeanPool.Monsky.translate_injective {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} : Function.Injective fun (a : ℝ) => translateTriangle a T

noncomputable def LeanPool.Monsky.zigPartCover (n : ℕ) : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))

The n translated copies of the scaled lower triangle Δ₀ covering the square.

Equations

• LeanPool.Monsky.zigPartCover n = Finset.image (fun (s : Fin n) => LeanPool.Monsky.translateTriangle (↑↑s / ↑n) (LeanPool.Monsky.scaleTriangle (1 / ↑n) LeanPool.Monsky.Δ₀)) Finset.univ

noncomputable def LeanPool.Monsky.zagPartCover (n : ℕ) : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))

The n translated copies of the scaled upper triangle Δ₀' covering the square.

Equations

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

theorem LeanPool.Monsky.zig_zag_cover_size_aux (n : ℕ) : (zigPartCover n).card = n ∧ (zagPartCover n).card = n

theorem LeanPool.Monsky.zig_zag_cover_size (n : ℕ) : (zigPartCover n ∪ zagPartCover n).card = 2 * n

theorem LeanPool.Monsky.zig_cover_area {n : ℕ} {Δ : Fin 3 → EuclideanSpace ℝ (Fin 2)} : Δ ∈ zigPartCover n → triangleArea Δ = 1 / (2 * ↑n)

theorem LeanPool.Monsky.zag_cover_area {n : ℕ} {Δ : Fin 3 → EuclideanSpace ℝ (Fin 2)} : Δ ∈ zagPartCover n → triangleArea Δ = 1 / (2 * ↑n)

theorem LeanPool.Monsky.fin_el_bound {n : ℕ} {x : ℝ} {s₁ s₂ : Fin n} (h₁l : x - 1 < ↑↑s₁) (h₁u : ↑↑s₁ < x) (h₂l : x - 1 < ↑↑s₂) (h₂u : ↑↑s₂ < x) : s₁ = s₂

theorem LeanPool.Monsky.zig_open_disjoint {n : ℕ} : disjointSet (↑(zigPartCover n)) openHull

theorem LeanPool.Monsky.zag_open_disjoint {n : ℕ} : disjointSet (↑(zagPartCover n)) openHull

theorem LeanPool.Monsky.zig_zag_open_disjoint {n : ℕ} (a₁ a₂ : Fin 3 → EuclideanSpace ℝ (Fin 2)) : a₁ ∈ zigPartCover n → a₂ ∈ zagPartCover n → Disjoint (openHull a₁) (openHull a₂)

theorem LeanPool.Monsky.zig_zag_covers_square {n : ℕ} (hn : n ≠ 0) : covers (↑(zigPartCover n) ∪ ↑(zagPartCover n)) (closedHull unitSquare) closedHull

theorem LeanPool.Monsky.monsky_easy_direction' {n : ℕ} (hn : Even n) (hnneq : n ≠ 0) : ∃ (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))), isEqualAreaCover (closedHull unitSquare) ↑S ∧ S.card = n