LeanPool.Monsky.SegmentTriangle

Imported Lean Pool material for LeanPool.Monsky.SegmentTriangle.

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

The determinant (signed area form) attached to a triangle's three vertices.

Equations

• LeanPool.Monsky.det T = ((T 0).ofLp 1 - (T 1).ofLp 1) * (T 2).ofLp 0 + ((T 1).ofLp 0 - (T 0).ofLp 0) * (T 2).ofLp 1 + ((T 0).ofLp 0 * (T 1).ofLp 1 - (T 1).ofLp 0 * (T 0).ofLp 1)

def LeanPool.Monsky.det₂ (x y : EuclideanSpace ℝ (Fin 2)) : ℝ

The 2×2 determinant of two plane vectors.

Equations

• LeanPool.Monsky.det₂ x y = x.ofLp 0 * y.ofLp 1 - x.ofLp 1 * y.ofLp 0

noncomputable def LeanPool.Monsky.segVec (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : EuclideanSpace ℝ (Fin 2)

The direction vector of a segment, from its first to its second endpoint.

Equations

• LeanPool.Monsky.segVec L = L 1 - L 0

def LeanPool.Monsky.signSeg (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) (v : EuclideanSpace ℝ (Fin 2)) : ℝ

The sign of the determinant of a triangle, as an element of ℝ.

Equations

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

def LeanPool.Monsky.toSegment (a b : EuclideanSpace ℝ (Fin 2)) : Fin 2 → EuclideanSpace ℝ (Fin 2)

The segment with the two given endpoints.

Equations

• LeanPool.Monsky.toSegment a b 0 = a
• LeanPool.Monsky.toSegment a b 1 = b

def LeanPool.Monsky.reverseSegment (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : Fin 2 → EuclideanSpace ℝ (Fin 2)

The segment with its two endpoints swapped.

Equations

• LeanPool.Monsky.reverseSegment L = LeanPool.Monsky.toSegment (L 1) (L 0)

def LeanPool.Monsky.colin (u v w : EuclideanSpace ℝ (Fin 2)) : Prop

colin u v w states that v lies strictly between the distinct points u and w.

Equations

• LeanPool.Monsky.colin u v w = (u ≠ w ∧ v ∈ LeanPool.Monsky.openHull (LeanPool.Monsky.toSegment u w))

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

The i-th side of a triangle, as a segment.

Equations

• LeanPool.Monsky.Tside T 0 = fun (x : Fin 2) => match x with | 0 => T 1 | 1 => T 2
• LeanPool.Monsky.Tside T 1 = fun (x : Fin 2) => match x with | 0 => T 2 | 1 => T 0
• LeanPool.Monsky.Tside T 2 = fun (x : Fin 2) => match x with | 0 => T 0 | 1 => T 1

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

The i-th barycentric coordinate of a point with respect to a triangle.

Equations

• LeanPool.Monsky.Tco T x i = LeanPool.Monsky.signSeg (LeanPool.Monsky.Tside T i) x / LeanPool.Monsky.det T

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

The opposite-side normal vector used in the barycentric coordinate formula.

Equations

• LeanPool.Monsky.Oside T i = LeanPool.Monsky.segVec (LeanPool.Monsky.Tside T i)

theorem LeanPool.Monsky.det₂_mul_last {x y : EuclideanSpace ℝ (Fin 2)} (a : ℝ) : det₂ x (a • y) = a * det₂ x y

theorem LeanPool.Monsky.aux_det₂ {L : EuclideanSpace ℝ (Fin 2)} (hL : L ≠ 0) (hi : ∃ (i : Fin 2), L.ofLp i = 0) : det₂ L (v 1 1) ≠ 0

theorem LeanPool.Monsky.open_segment_sub {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hsub : ∀ (i : Fin 2), L₁ i ∈ closedHull L₂) (hL₁ : L₁ 0 ≠ L₁ 1) : openHull L₁ ⊆ openHull L₂

theorem LeanPool.Monsky.open_segment_sub' {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hsub : closedHull L₁ ⊆ closedHull L₂) (hL₁ : L₁ 0 ≠ L₁ 1) : openHull L₁ ⊆ openHull L₂

theorem LeanPool.Monsky.boundary_seg {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L 0 ≠ L 1) : boundary L = ↑(Finset.image (fun (i : Fin 2) => L i) Finset.univ)

theorem LeanPool.Monsky.boundary_seg' {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L 0 ≠ L 1) (i : Fin 2) : L i ∈ boundary L

theorem LeanPool.Monsky.boundary_seg_set {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L 0 ≠ L 1) : boundary L = {L 0, L 1}

theorem LeanPool.Monsky.boundary_seg_nonempty {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary L) : L 0 ≠ L 1

theorem LeanPool.Monsky.signSeg_line (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) (x y : EuclideanSpace ℝ (Fin 2)) (a : ℝ) : signSeg L (x + a • y) = signSeg L x + a * det₂ (segVec L) y

theorem LeanPool.Monsky.segVec_zero_iff (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : segVec L = 0 ↔ L 0 = L 1

theorem LeanPool.Monsky.segVec_nonzero_iff (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : segVec L ≠ 0 ↔ L 0 ≠ L 1

theorem LeanPool.Monsky.closed_segment_interval_im {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : closedHull L = (fun (a : ℝ) => L 0 + a • segVec L) '' Set.Icc 0 1

theorem LeanPool.Monsky.open_segment_interval_im {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : openHull L = (fun (a : ℝ) => L 0 + a • segVec L) '' Set.Ioo 0 1

theorem LeanPool.Monsky.segVec_zero_closedHull {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : segVec L = 0) : closedHull L = {L 0}

theorem LeanPool.Monsky.segVec_zero_openHull {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : segVec L = 0) : openHull L = {L 0}

theorem LeanPool.Monsky.seg_dir_sub {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hxL : x ∈ openHull L) : ∃ δ > 0, ∀ (a : ℝ), |a| ≤ δ → x + a • segVec L ∈ openHull L

theorem LeanPool.Monsky.segVec_co {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {x y : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull L) (hy : y ∈ closedHull L) : ∃ (a : ℝ), y = x + a • segVec L

theorem LeanPool.Monsky.open_seg_nonempty (L : Fin 2 → EuclideanSpace ℝ (Fin 2)) : ∃ (x : EuclideanSpace ℝ (Fin 2)), x ∈ openHull L

theorem LeanPool.Monsky.perp_vec_exists (Lset : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))) (hLset : ∀ L ∈ Lset, L 0 ≠ L 1) : ∃ (y : EuclideanSpace ℝ (Fin 2)), ∀ L ∈ Lset, det₂ (segVec L) y ≠ 0

@[simp]

theorem LeanPool.Monsky.segment_rfl {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : toSegment (L 0) (L 1) = L

@[simp]

theorem LeanPool.Monsky.reverseSegment_toSegment {u v : EuclideanSpace ℝ (Fin 2)} : reverseSegment (toSegment u v) = toSegment v u

@[simp]

theorem LeanPool.Monsky.reverseSegment_involution {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : reverseSegment (reverseSegment L) = L

theorem LeanPool.Monsky.reverseSegment_bijective : Function.Bijective reverseSegment

theorem LeanPool.Monsky.reverseSegment_closedHull {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : closedHull (reverseSegment L) = closedHull L

theorem LeanPool.Monsky.reverseSegment_openHull {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : openHull (reverseSegment L) = openHull L

theorem LeanPool.Monsky.reverseSegment_boundary {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : boundary (reverseSegment L) = boundary L

theorem LeanPool.Monsky.segment_triv {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : L 0 = L 1 ↔ ∃ (x : EuclideanSpace ℝ (Fin 2)), closedHull L = {x}

theorem LeanPool.Monsky.segment_triv' {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : L 0 = L 1 ↔ closedHull L = {L 0}

theorem LeanPool.Monsky.seg_nontriv_sub {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : closedHull L₁ ⊆ closedHull L₂) (hneq : L₁ 0 ≠ L₁ 1) : L₂ 0 ≠ L₂ 1

def LeanPool.Monsky.lastIndex : Fin 3 → Fin 3 → Fin 3

The remaining index of Fin 3 distinct from two given indices.

Equations

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

theorem LeanPool.Monsky.linearCombinationDetLast {n : ℕ} {x y : EuclideanSpace ℝ (Fin 2)} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {α : Fin n → ℝ} (hα : ∑ i : Fin n, α i = 1) : (det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => y | 2 => ∑ i : Fin n, α i • P i) = ∑ i : Fin n, α i * det fun (x_1 : Fin 3) => match x_1 with | 0 => x | 1 => y | 2 => P i

theorem LeanPool.Monsky.Tco_sum {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (x : EuclideanSpace ℝ (Fin 2)) : ∑ i : Fin 3, Tco T x i = 1

theorem LeanPool.Monsky.Tco_linear {n : ℕ} {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {α : Fin n → ℝ} (hα : ∑ i : Fin n, α i = 1) (k : Fin 3) : Tco T (∑ i : Fin n, α i • P i) k = ∑ i : Fin n, α i * Tco T (P i) k

theorem LeanPool.Monsky.Tco_basis_diag {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {i : Fin 3} : Tco T (T i) i = 1

theorem LeanPool.Monsky.Tco_basis_off_diag {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {i j : Fin 3} (hij : i ≠ j) : Tco T (T i) j = 0

theorem LeanPool.Monsky.Tco_sum_val {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {α : Fin 3 → ℝ} (hα : ∑ i : Fin 3, α i = 1) (k : Fin 3) : Tco T (∑ i : Fin 3, α i • T i) k = α k

theorem LeanPool.Monsky.Tco_sum_self {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (x : EuclideanSpace ℝ (Fin 2)) : ∑ i : Fin 3, Tco T x i • T i = x

theorem LeanPool.Monsky.closed_triangle_iff {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} : x ∈ closedHull T ↔ ∀ (i : Fin 3), 0 ≤ Tco T x i

theorem LeanPool.Monsky.open_triangle_iff {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} : x ∈ openHull T ↔ ∀ (i : Fin 3), 0 < Tco T x i

theorem LeanPool.Monsky.two_co_zero_imp_corner_co {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {i j : Fin 3} {x : EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (hij : i ≠ j) (hi : Tco T x i = 0) (hj : Tco T x j = 0) : Tco T x (lastIndex i j) = 1

theorem LeanPool.Monsky.two_co_zero_imp_corner {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {i j : Fin 3} {x : EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (hij : i ≠ j) (hi : Tco T x i = 0) (hj : Tco T x j = 0) : x = T (lastIndex i j)

theorem LeanPool.Monsky.Tco_line {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (x y : EuclideanSpace ℝ (Fin 2)) (a : ℝ) : Tco T (x + a • y) i = Tco T x i + a * det₂ (Oside T i) y / det T

theorem LeanPool.Monsky.nondegen_triangle_imp_nondegen_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (i : Fin 3) (hdet : det T ≠ 0) : Tside T i 0 ≠ Tside T i 1

theorem LeanPool.Monsky.mem_closed_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull T) (i : Fin 3) : Tco T x i = 0 ↔ x ∈ closedHull (Tside T i)

theorem LeanPool.Monsky.closed_side_sub {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (hx : x ∈ closedHull (Tside T i)) : x ∈ closedHull T

theorem LeanPool.Monsky.closed_side_sub' {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {i : Fin 3} : closedHull (Tside T i) ⊆ closedHull T

theorem LeanPool.Monsky.closed_side_to_co {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (hx : x ∈ closedHull (Tside T i)) : Tco T x i = 0

theorem LeanPool.Monsky.mem_open_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull T) (i : Fin 3) : (Tco T x i = 0 ∧ ∀ (j : Fin 3), j ≠ i → 0 < Tco T x j) ↔ x ∈ openHull (Tside T i)

theorem LeanPool.Monsky.mem_open_side_other_co {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (hxOpen : x ∈ openHull (Tside T i)) (j : Fin 3) : j ≠ i → 0 < Tco T x j

theorem LeanPool.Monsky.boundary_iff {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull T) : x ∈ boundary T ↔ ∃ (i : Fin 3), Tco T x i = 0

theorem LeanPool.Monsky.side_in_boundary {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (i : Fin 3) : closedHull (Tside T i) ⊆ boundary T

theorem LeanPool.Monsky.boundary_is_union_sides {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) : boundary T = ⋃ (i : Fin 3), closedHull (Tside T i)

theorem LeanPool.Monsky.el_boundary_imp_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ boundary T) : ∃ (i : Fin 3), x ∈ closedHull (Tside T i)

theorem LeanPool.Monsky.el_in_boundary_imp_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (hx : x ∈ boundary T) (hv : ∀ (i : Fin 3), x ≠ T i) : ∃ (i : Fin 3), x ∈ openHull (Tside T i)

theorem LeanPool.Monsky.seg_inter_open {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {x y : EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (hxT : x ∈ openHull (Tside T i)) (hdet : det T ≠ 0) (hdet₂ : det₂ (segVec (Tside T i)) y ≠ 0) : ∃ σ ∈ {-1, 1}, (∃ δ > 0, ∀ (a : ℝ), 0 < a → a ≤ δ → x + a • σ • y ∈ openHull T) ∧ ∀ (a : ℝ), 0 < a → x + a • -σ • y ∉ closedHull T

theorem LeanPool.Monsky.seg_sub_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} {i : Fin 3} (hdet : det T ≠ 0) (hxL : x ∈ openHull L) (hxT : x ∈ openHull (Tside T i)) (hInter : openHull T ∩ closedHull L = ∅) (hv : ∀ (i : Fin 3), T i ∉ openHull L) : closedHull L ⊆ closedHull (Tside T i)

theorem LeanPool.Monsky.segment_in_boundary_imp_in_side {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) (hL : closedHull L ⊆ boundary T) : ∃ (i : Fin 3), closedHull L ⊆ closedHull (Tside T i)

theorem LeanPool.Monsky.closed_triangle_is_closed_dir {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hdet : det T ≠ 0) {x y : EuclideanSpace ℝ (Fin 2)} (h : {n : ℕ | x + (1 / ↑n) • y ∈ closedHull T}.Infinite) : x ∈ closedHull T

theorem LeanPool.Monsky.colin_reverse {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) : colin w v u

theorem LeanPool.Monsky.colin_decomp_closed {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) : closedHull (toSegment u w) = closedHull (toSegment u v) ∪ closedHull (toSegment v w)

theorem LeanPool.Monsky.middle_not_boundary_colin {u v w : EuclideanSpace ℝ (Fin 2)} (hcolin : colin u v w) : u ≠ v ∧ v ≠ w

theorem LeanPool.Monsky.left_openHull_in_colin {u v w : EuclideanSpace ℝ (Fin 2)} {h : colin u v w} : openHull (toSegment u v) ⊆ openHull (toSegment u w)

theorem LeanPool.Monsky.right_openHull_in_colin {u v w : EuclideanSpace ℝ (Fin 2)} {h : colin u v w} : openHull (toSegment v w) ⊆ openHull (toSegment u w)

theorem LeanPool.Monsky.interior_left_trans {u v w t : EuclideanSpace ℝ (Fin 2)} (ht : t ∈ openHull (toSegment u v)) (hv : v ∈ openHull (toSegment u w)) : t ∈ openHull (toSegment u w)

noncomputable def LeanPool.Monsky.makeNewTwoSimplex (a b : Fin 2 → ℝ) : Fin 2 → ℝ

The two-simplex used to express a point of one segment inside another.

Equations

• LeanPool.Monsky.makeNewTwoSimplex a b 0 = a 0 / (1 - a 1 * b 0)
• LeanPool.Monsky.makeNewTwoSimplex a b 1 = a 1 * b 1 / (1 - a 1 * b 0)

theorem LeanPool.Monsky.makeNewTwoSimplex_lem (a b : Fin 2 → ℝ) (ha_simplex : a ∈ openSimplex 2) (hb_simplex : b ∈ openSimplex 2) : makeNewTwoSimplex a b ∈ openSimplex 2

theorem LeanPool.Monsky.two_colin_in_openHull {u v w x : EuclideanSpace ℝ (Fin 2)} (h₁ : colin u v w) (h₂ : colin v w x) : v ∈ openHull (toSegment u x)

theorem LeanPool.Monsky.colin_trans_right {u v w x : EuclideanSpace ℝ (Fin 2)} (h₁ : colin u v w) (h₂ : colin v w x) : colin u w x

theorem LeanPool.Monsky.colin_trans_left {u v w x : EuclideanSpace ℝ (Fin 2)} (h₁ : colin u v w) (h₂ : colin v w x) : colin u v x

theorem LeanPool.Monsky.sub_collinear_left {u v w t : EuclideanSpace ℝ (Fin 2)} (hc : colin u v w) (ht : t ∈ openHull (toSegment u v)) : colin u t v

theorem LeanPool.Monsky.sub_collinear_right {u v w t : EuclideanSpace ℝ (Fin 2)} (hc : colin u v w) (ht : t ∈ openHull (toSegment u v)) : colin t v w

theorem LeanPool.Monsky.sub_collinear_right' {u v w t : EuclideanSpace ℝ (Fin 2)} (hc : colin u v w) (ht : t ∈ closedHull (toSegment u v)) (htv : t ≠ v) : colin t v w

theorem LeanPool.Monsky.closed_in_clopen_right {v z w : EuclideanSpace ℝ (Fin 2)} (hvw : v ≠ w) (hz : z ∈ closedHull (toSegment v w) \ {v}) : closedHull (toSegment z w) ⊆ closedHull (toSegment v w) \ {v}

theorem LeanPool.Monsky.corrollary_closed_in_clopen_right {v z w : EuclideanSpace ℝ (Fin 2)} (hclop : closedHull (toSegment z w) ⊆ closedHull (toSegment v w) \ {v}) : v ∉ closedHull (toSegment z w)

theorem LeanPool.Monsky.middle_intersection_empty {u v w : EuclideanSpace ℝ (Fin 2)} {h : colin u v w} : closedHull (toSegment u v) ∩ (closedHull (toSegment v w) \ {v}) = ∅

theorem LeanPool.Monsky.colin_intersection_openHulls_empty {u v w : EuclideanSpace ℝ (Fin 2)} {h : colin u v w} : openHull (toSegment u v) ∩ openHull (toSegment v w) = ∅

theorem LeanPool.Monsky.clopen_left {u v w : EuclideanSpace ℝ (Fin 2)} {h : colin u v w} : closedHull (toSegment u w) \ closedHull (toSegment u v) = closedHull (toSegment v w) \ {v}

theorem LeanPool.Monsky.sub_collinear_right_symm' {u v w t : EuclideanSpace ℝ (Fin 2)} (hc : colin u v w) (ht : t ∈ closedHull (toSegment v w)) (htv : t ≠ v) : colin u v t

theorem LeanPool.Monsky.colin_sub_aux {u v w x : EuclideanSpace ℝ (Fin 2)} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hc : colin u v w) (hLsub : closedHull L ⊆ closedHull (toSegment u w)) (hv : v ∉ openHull L) (hxL : x ∈ openHull L) (hx : x ∈ closedHull (toSegment u v)) : closedHull L ⊆ closedHull (toSegment u v)

def LeanPool.Monsky.ClosedSymSeg : Sym2 (EuclideanSpace ℝ (Fin 2)) → Set (EuclideanSpace ℝ (Fin 2))

The closed hull of the segment associated to an unordered pair of points.

Equations

• LeanPool.Monsky.ClosedSymSeg = Sym2.lift ⟨fun (a b : EuclideanSpace ℝ (Fin 2)) => LeanPool.Monsky.closedHull (LeanPool.Monsky.toSegment a b), LeanPool.Monsky.ClosedSymSeg._proof_1⟩

theorem LeanPool.Monsky.colin_sub {u v w : EuclideanSpace ℝ (Fin 2)} (h : colin u v w) {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hLsub : closedHull L ⊆ closedHull (toSegment u w)) (hLv : v ∉ openHull L) : closedHull L ⊆ closedHull (toSegment u v) ∨ closedHull L ⊆ closedHull (toSegment v w)

theorem LeanPool.Monsky.closedHull_eq_imp_eq_triv {u v x y : EuclideanSpace ℝ (Fin 2)} (huv : u = v) (h : closedHull (toSegment u v) = closedHull (toSegment x y)) : u = x ∧ u = y

theorem LeanPool.Monsky.closedHull_eq_imp_eq_or_rev_seg_aux {u v x y : EuclideanSpace ℝ (Fin 2)} (h : closedHull (toSegment u v) = closedHull (toSegment x y)) : u = x ∨ u = y

theorem LeanPool.Monsky.closedHull_eq_imp_eq_or_rev_seg {u v x y : EuclideanSpace ℝ (Fin 2)} (h : closedHull (toSegment u v) = closedHull (toSegment x y)) : u = x ∧ v = y ∨ u = y ∧ v = x

theorem LeanPool.Monsky.closedHull_eq_imp_eq_or_rev {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : closedHull L₁ = closedHull L₂) : L₁ = L₂ ∨ L₁ = reverseSegment L₂

theorem LeanPool.Monsky.closedHull_eq_imp_openHull_eq {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : closedHull L₁ = closedHull L₂) : openHull L₁ = openHull L₂

theorem LeanPool.Monsky.closedHull_eq_imp_boundary_eq {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : closedHull L₁ = closedHull L₂) : boundary L₁ = boundary L₂

noncomputable def LeanPool.Monsky.linePar (v₁ v₂ : EuclideanSpace ℝ (Fin 2)) : ℝ → EuclideanSpace ℝ (Fin 2)

The parametrization of the line through v₁ in direction v₂.

Equations

• LeanPool.Monsky.linePar v₁ v₂ t = v₁ + t • v₂

theorem LeanPool.Monsky.seg_par_injective {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (h : v₂ ≠ 0) : Function.Injective (linePar v₁ v₂)

theorem LeanPool.Monsky.seg_par₀ {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} : linePar v₁ v₂ 0 = v₁

theorem LeanPool.Monsky.seg_par_closed_self {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : closedHull L = linePar (L 0) (segVec L) '' Set.Icc 0 1

theorem LeanPool.Monsky.seg_par_open_self {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} : openHull L = linePar (L 0) (segVec L) '' Set.Ioo 0 1

theorem LeanPool.Monsky.linePar_scalar_Icc {a b t : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (ht : 0 < t) : linePar v₁ (t • v₂) '' Set.Icc a b = linePar v₁ v₂ '' Set.Icc (t * a) (t * b)

theorem LeanPool.Monsky.linePar_neg {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} : linePar v₁ v₂ '' Set.Icc a b = linePar v₁ (-v₂) '' Set.Icc (-b) (-a)

theorem LeanPool.Monsky.linePar_scalar_Icc' {a b t : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (ht : t < 0) : linePar v₁ (t • v₂) '' Set.Icc a b = linePar v₁ v₂ '' Set.Icc (t * b) (t * a)

theorem LeanPool.Monsky.linePar_trans_Icc {a b t : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} : linePar (v₁ + t • v₂) v₂ '' Set.Icc a b = linePar v₁ v₂ '' Set.Icc (a + t) (b + t)

theorem LeanPool.Monsky.linePar_closed {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (hab : a ≤ b) : linePar v₁ v₂ '' Set.Icc a b = closedHull (toSegment (v₁ + a • v₂) (v₁ + b • v₂))

theorem LeanPool.Monsky.linePar_open {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (hab : a < b) : linePar v₁ v₂ '' Set.Ioo a b = openHull (toSegment (v₁ + a • v₂) (v₁ + b • v₂))

theorem LeanPool.Monsky.segVec_mul {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : closedHull L₁ ⊆ closedHull L₂) : ∃ (t : ℝ), segVec L₁ = t • segVec L₂

theorem LeanPool.Monsky.seg_par {L₁ L₂ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h₁ : L₁ 0 ≠ L₁ 1) (h₂ : closedHull L₁ ⊆ closedHull L₂) : ∃ (a : ℝ) (b : ℝ), closedHull L₂ = linePar (L₁ 0) (segVec L₁) '' Set.Icc a b

theorem LeanPool.Monsky.seg_par_openHull {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (hab : a < b) (hc : closedHull L = linePar v₁ v₂ '' Set.Icc a b) : openHull L = linePar v₁ v₂ '' Set.Ioo a b

theorem LeanPool.Monsky.seg_par_boundary {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (hab : a < b) (h : v₂ ≠ 0) (hc : closedHull L = linePar v₁ v₂ '' Set.Icc a b) : boundary L = linePar v₁ v₂ '' {a, b}

theorem LeanPool.Monsky.seg_par_nontrivial {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} {a b : ℝ} {v₁ v₂ : EuclideanSpace ℝ (Fin 2)} (hL : L 0 ≠ L 1) (hc : closedHull L = linePar v₁ v₂ '' Set.Icc a b) : a < b

theorem LeanPool.Monsky.interval_intersection {a₁ a₂ b₁ b₂ : ℝ} (hx₁ : Set.Icc 0 1 ⊆ Set.Icc a₁ b₁) (hx₂ : Set.Icc 0 1 ⊆ Set.Icc a₂ b₂) (ha : a₂ ∉ Set.Ioo a₁ b₁) (hb : b₂ ∉ Set.Ioo a₁ b₁) : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂

theorem LeanPool.Monsky.seg_sub_seg {L₁ L₂ L₃ : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h₁ : L₁ 0 ≠ L₁ 1) (h₂ : closedHull L₁ ⊆ closedHull L₂) (h₃ : closedHull L₁ ⊆ closedHull L₃) (h₂₃ : Disjoint (openHull L₂) (boundary L₃)) : closedHull L₂ ⊆ closedHull L₃

theorem LeanPool.Monsky.seg_openHull_infinite {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : L 0 ≠ L 1) : (openHull L).Infinite

theorem LeanPool.Monsky.seg_closedHull_infinite {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (h : L 0 ≠ L 1) : (closedHull L).Infinite

theorem LeanPool.Monsky.closed_segment_sub_union_segment {A : Finset (Fin 2 → EuclideanSpace ℝ (Fin 2))} {L : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hL : L 0 ≠ L 1) (hSub : closedHull L ⊆ ⋃ S ∈ A, closedHull S) (hA : ∀ S ∈ A, Disjoint (openHull L) (boundary S)) : ∃ S ∈ A, closedHull L ⊆ closedHull S

theorem LeanPool.Monsky.openHull_convex {n : ℕ} {P : Fin n → EuclideanSpace ℝ (Fin 2)} {x y : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ openHull P) (hy : y ∈ openHull P) : closedHull (toSegment x y) ⊆ openHull P

theorem LeanPool.Monsky.open_sub_closed_sub (S L : Fin 2 → EuclideanSpace ℝ (Fin 2)) (h : openHull S ⊆ openHull L) : closedHull S ⊆ closedHull L

noncomputable def LeanPool.Monsky.segmentAroundX (x y : EuclideanSpace ℝ (Fin 2)) (ε₁ ε₂ : ℝ) : Fin 2 → EuclideanSpace ℝ (Fin 2)

A small segment centered at x in the direction of a given vector.

Equations

• LeanPool.Monsky.segmentAroundX x y ε₁ ε₂ = LeanPool.Monsky.toSegment (x + (1 * ε₁) • y) (x + (-1 * ε₂) • y)

theorem LeanPool.Monsky.openHull_segment_around {x y : EuclideanSpace ℝ (Fin 2)} {ε₁ ε₂ : ℝ} (h₁ : 0 < ε₁) (h₂ : 0 < ε₂) : x ∈ openHull (segmentAroundX x y ε₁ ε₂)

theorem LeanPool.Monsky.openHull_segment_around_non_trivial {x y : EuclideanSpace ℝ (Fin 2)} {ε₁ ε₂ : ℝ} (hy : y ≠ 0) (hε : ε₁ + ε₂ ≠ 0) : segVec (segmentAroundX x y ε₁ ε₂) ≠ 0

theorem LeanPool.Monsky.real_number_bound_aux {n : ℕ} {f g : Fin n → ℝ} (h₁ : ∀ (i : Fin n), 0 < f i) (h₂ : ∀ ε > 0, ∃ (i : Fin n), ε * g i ≤ -f i) : False

theorem LeanPool.Monsky.triangle_openHull_open {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hnonDeg : det T ≠ 0) {x : EuclideanSpace ℝ (Fin 2)} (y : EuclideanSpace ℝ (Fin 2)) (hx : x ∈ openHull T) : ∃ ε > 0, x + ε • y ∈ openHull T

theorem LeanPool.Monsky.triangle_direction_sub {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull T) (hn : ∀ (i : Fin 3), x ≠ T i) : ∃ (L : Fin 2 → EuclideanSpace ℝ (Fin 2)), L 0 ≠ L 1 ∧ x ∈ openHull L ∧ closedHull L ⊆ closedHull T

theorem LeanPool.Monsky.inward_pointing_vector_exists {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {x : EuclideanSpace ℝ (Fin 2)} (hx : x ∈ closedHull T) (hT : ¬∀ (i j : Fin 3), T i = T j) : ∃ (y : EuclideanSpace ℝ (Fin 2)), x ≠ y ∧ openHull (toSegment x y) ⊆ openHull T

theorem LeanPool.Monsky.seg_inter_open_triangle {T : Fin 3 → EuclideanSpace ℝ (Fin 2)} {S : Fin 2 → EuclideanSpace ℝ (Fin 2)} (hDet : det T ≠ 0) (hST : closedHull S ∩ openHull T ≠ ∅) : openHull S ∩ openHull T ≠ ∅

theorem LeanPool.Monsky.disjoint_opens_implies_disjoint_open_closed {T₁ T₂ : Fin 3 → EuclideanSpace ℝ (Fin 2)} (hT : Disjoint (openHull T₁) (openHull T₂)) (hDet : det T₂ ≠ 0) : Disjoint (closedHull T₁) (openHull T₂)