LeanPool.Monsky.Square

Imported Lean Pool material for LeanPool.Monsky.Square.

def LeanPool.Monsky.unitSquare : Fin 4 → EuclideanSpace ℝ (Fin 2)

The unit square as a four-vertex polygon.

Equations

• LeanPool.Monsky.unitSquare 0 = LeanPool.Monsky.v 0 0
• LeanPool.Monsky.unitSquare 1 = LeanPool.Monsky.v 1 0
• LeanPool.Monsky.unitSquare 2 = LeanPool.Monsky.v 1 1
• LeanPool.Monsky.unitSquare 3 = LeanPool.Monsky.v 0 1

theorem LeanPool.Monsky.closed_unitSquare_eq : closedHull unitSquare = {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), 0 ≤ x.ofLp i ∧ x.ofLp i ≤ 1}

theorem LeanPool.Monsky.open_unitSquare_eq : openHull unitSquare = {x : EuclideanSpace ℝ (Fin 2) | ∀ (i : Fin 2), 0 < x.ofLp i ∧ x.ofLp i < 1}

theorem LeanPool.Monsky.element_in_boundary_square {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary unitSquare) : ∃ (i : Fin 2), x.ofLp i = 0 ∨ x.ofLp i = 1

theorem LeanPool.Monsky.boundary_unitSquare_eq : boundary unitSquare = {x : EuclideanSpace ℝ (Fin 2) | (∀ (i : Fin 2), 0 ≤ x.ofLp i ∧ x.ofLp i ≤ 1) ∧ ∃ (i : Fin 2), x.ofLp i = 0 ∨ x.ofLp i = 1}

theorem LeanPool.Monsky.segment_in_boundary_square {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary unitSquare) : ∃ (i : Fin 2), ∀ (L : Fin 2 → EuclideanSpace ℝ (Fin 2)), x ∈ openHull L → closedHull L ⊆ closedHull unitSquare → (segVec L).ofLp i = 0

theorem LeanPool.Monsky.open_unitSquare_open_dir {x : EuclideanSpace ℝ (Fin 2)} (y : EuclideanSpace ℝ (Fin 2)) (hx : x ∈ openHull unitSquare) : ∃ ε > 0, ∀ (n : ℕ), x + (1 / ↑n) • ε • y ∈ openHull unitSquare

theorem LeanPool.Monsky.el_boundary_square_triangle_dir {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary unitSquare) : ∃ σ ∈ {-1, 1}, ∀ (Δ : Fin 3 → EuclideanSpace ℝ (Fin 2)), det Δ ≠ 0 → closedHull Δ ⊆ closedHull unitSquare → (∃ (i : Fin 3), x ∈ openHull (Tside Δ i)) → ∃ εΔ > 0, ∀ (y : ℝ), 0 < y → y ≤ εΔ → x + (σ * y) • v 1 1 ∈ openHull Δ

theorem LeanPool.Monsky.boundary_leave_dir {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary unitSquare) : ∃ σ ∈ {1, -1}, ∀ ε > 0, x + (σ * ε) • v 1 1 ∉ closedHull unitSquare

theorem LeanPool.Monsky.segment_triangle_pairing_int (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hCover : isDisjointCover (closedHull unitSquare) ↑S) (hArea : ∀ Δ ∈ S, det Δ ≠ 0) (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) (hInt : ∀ Δ ∈ S, openHull Δ ∩ closedHull L = ∅) (hLunit : openHull L ⊆ openHull unitSquare) (hv : ∀ Δ ∈ S, ∀ (i : Fin 3), Δ i ∉ openHull L) : {Δ ∈ S | closedHull L ⊆ boundary Δ}.card = 2

theorem LeanPool.Monsky.segment_triangle_pairing_boundary (S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))) (hCover : isDisjointCover (closedHull unitSquare) ↑S) (hArea : ∀ Δ ∈ S, det Δ ≠ 0) (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) (hL : L 0 ≠ L 1) (hInt : ∀ Δ ∈ S, openHull Δ ∩ closedHull L = ∅) (hLunit : openHull L ⊆ boundary unitSquare) (hv : ∀ Δ ∈ S, ∀ (i : Fin 3), Δ i ∉ openHull L) : {Δ ∈ S | closedHull L ⊆ boundary Δ}.card = 1

def LeanPool.Monsky.squareBoundaryBig : Fin 4 → Fin 2 → EuclideanSpace ℝ (Fin 2)

The i-th side of the unit square, as a segment.

Equations

• LeanPool.Monsky.squareBoundaryBig 0 = fun (x : Fin 2) => match x with | 0 => LeanPool.Monsky.v 0 0 | 1 => LeanPool.Monsky.v 1 0
• LeanPool.Monsky.squareBoundaryBig 1 = fun (x : Fin 2) => match x with | 0 => LeanPool.Monsky.v 1 0 | 1 => LeanPool.Monsky.v 1 1
• LeanPool.Monsky.squareBoundaryBig 2 = fun (x : Fin 2) => match x with | 0 => LeanPool.Monsky.v 1 1 | 1 => LeanPool.Monsky.v 0 1
• LeanPool.Monsky.squareBoundaryBig 3 = fun (x : Fin 2) => match x with | 0 => LeanPool.Monsky.v 0 1 | 1 => LeanPool.Monsky.v 0 0

noncomputable def LeanPool.Monsky.squareBoundaryBigSet : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))

The four sides of the unit square, as a set of segments.

Equations

• LeanPool.Monsky.squareBoundaryBigSet = ⊤.biUnion fun (i : Fin 4) => {LeanPool.Monsky.squareBoundaryBig i}

theorem LeanPool.Monsky.squareBoundaryBig_corners (i : Fin 4) (j : Fin 2) : ∃ (k : Fin 4), squareBoundaryBig i j = unitSquare k

theorem LeanPool.Monsky.squareBoundaryBig_injective : Function.Injective squareBoundaryBig

theorem LeanPool.Monsky.square_boundary_sides_nonDegen (i : Fin 4) : squareBoundaryBig i 0 ≠ squareBoundaryBig i 1

def LeanPool.Monsky.boundaryLine : Fin 4 → Fin 2

The index of the coordinate that is constant along side i of the square.

Equations

• LeanPool.Monsky.boundaryLine 0 = 0
• LeanPool.Monsky.boundaryLine 1 = 1
• LeanPool.Monsky.boundaryLine 2 = 0
• LeanPool.Monsky.boundaryLine 3 = 1

def LeanPool.Monsky.bc : Fin 4 → ℝ

The constant coordinate value along side i of the unit square.

Equations

• LeanPool.Monsky.bc 0 = 0
• LeanPool.Monsky.bc 1 = 1
• LeanPool.Monsky.bc 2 = 1
• LeanPool.Monsky.bc 3 = 0

@[simp]

theorem LeanPool.Monsky.boundaryLine_rw {i : Fin 4} : boundaryLine i = (fun (x : Fin 4) => match x with | 0 => 0 | 1 => 1 | 2 => 0 | 3 => 1) i

@[simp]

theorem LeanPool.Monsky.boundary_constant_rw {i : Fin 4} : bc i = (fun (x : Fin 4) => match x with | 0 => 0 | 1 => 1 | 2 => 1 | 3 => 0) i

theorem LeanPool.Monsky.squareBoundaryBig_eq (i : Fin 4) : closedHull (squareBoundaryBig i) = {x : EuclideanSpace ℝ (Fin 2) | 0 ≤ x.ofLp (boundaryLine i) ∧ x.ofLp (boundaryLine i) ≤ 1 ∧ x.ofLp (boundaryLine i + 1) = bc i}

theorem LeanPool.Monsky.square_boundary_in_boundary (i : Fin 4) : closedHull (squareBoundaryBig i) ⊆ boundary unitSquare

theorem LeanPool.Monsky.square_boundary_segments_in_boundary (i : Fin 4) : closedHull (squareBoundaryBig i) ⊆ boundary unitSquare

theorem LeanPool.Monsky.boundary_in_square_boundary {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary unitSquare) : ∃ (i : Fin 4), x ∈ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.square_boundary_is_union_sides : boundary unitSquare = ⋃ (i : Fin 4), closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.squareBoundaryBig_inter_seg_aux₁ {a b c d : ℝ} (ha : 0 < a) (hb : 0 ≤ b) (hc : 0 < c) (hd : 0 ≤ d) (habcd : a * b + c * d = 0) : b = 0 ∧ d = 0

theorem LeanPool.Monsky.squareBoundaryBig_inter_seg_aux₂ {a b c d : ℝ} (hac : a + c = 1) (ha : 0 < a) (hb : b ≤ 1) (hc : 0 < c) (hd : d ≤ 1) (habcd : a * b + c * d = 1) : b = 1 ∧ d = 1

theorem LeanPool.Monsky.squareBoundaryBig_inter_seg {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} {i : Fin 4} (hx : x ∈ openHull S) (hxi : x ∈ closedHull (squareBoundaryBig i)) (hS : closedHull S ⊆ closedHull unitSquare) : closedHull S ⊆ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.convex_faces {x y p : EuclideanSpace ℝ (Fin 2)} (i : Fin 4) (hpiface : p ∈ closedHull (squareBoundaryBig i)) (hp : p ∈ openHull (toSegment x y)) (hx : x ∈ closedHull unitSquare) (hy : y ∈ closedHull unitSquare) : x ∈ closedHull (squareBoundaryBig i) ∧ y ∈ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.convex_faces'' {p : EuclideanSpace ℝ (Fin 2)} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (i : Fin 4) (hpiface : p ∈ closedHull (squareBoundaryBig i)) (hp : p ∈ openHull L) (hx : L 0 ∈ closedHull unitSquare) (hy : L 1 ∈ closedHull unitSquare) : closedHull L ⊆ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.square_boundary_pairwise_inter {i : Fin 4} : closedHull (squareBoundaryBig (i - 1)) ∩ closedHull (squareBoundaryBig i) = {unitSquare i}

theorem LeanPool.Monsky.square_corner_in_boundary {i : Fin 4} : unitSquare i ∈ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.square_corner_in_boundary' {i : Fin 4} : unitSquare i ∈ closedHull (squareBoundaryBig (i - 1))

theorem LeanPool.Monsky.segment_through_corner {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} {i : Fin 4} (hx : unitSquare i ∈ openHull S) (hS : closedHull S ⊆ closedHull unitSquare) : closedHull S = {unitSquare i}

theorem LeanPool.Monsky.cover_imples_corner_in_triangle {S : Finset (Fin 3 → EuclideanSpace ℝ (Fin 2))} (hCover : isCover (closedHull unitSquare) ↑S) (i : Fin 4) : ∃ T ∈ S, ∃ (j : Fin 3), unitSquare i = T j

theorem LeanPool.Monsky.line_in_boundary {x : EuclideanSpace ℝ (Fin 2)} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : closedHull L ⊆ closedHull unitSquare) (hboundary : x ∈ openHull L ∩ boundary unitSquare) : closedHull L ⊆ boundary unitSquare

theorem LeanPool.Monsky.unitSquare_is_convex {x y : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull unitSquare) (hy : y ∈ closedHull unitSquare) : closedHull (toSegment x y) ⊆ closedHull unitSquare

theorem LeanPool.Monsky.unitSquare_is_convex' {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : closedHull S ⊆ boundary unitSquare) : ∃ (i : Fin 4), closedHull S ⊆ closedHull (squareBoundaryBig i)

theorem LeanPool.Monsky.unitSquare_is_convex_open {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : closedHull S ⊆ boundary unitSquare) (hNondegen : S 0 ≠ S 1) : ∃ (i : Fin 4), openHull S ⊆ openHull (squareBoundaryBig i)

theorem LeanPool.Monsky.openHull_segment_in_boundary {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hS : openHull S ⊆ boundary unitSquare) (hcS : closedHull S ⊆ closedHull unitSquare) : ∃ (i : Fin 4), closedHull S ⊆ closedHull (squareBoundaryBig i)