inductive Set.collinearTriple {V : Type u_1} [MetricSpace V] : Set V → Prop

• mk {V : Type u_1} [MetricSpace V] {u v w : V} (h : sbtw u v w) : {u, v, w}.collinearTriple

theorem Set.collinearTriple_iff {V : Type u_1} [MetricSpace V] (a✝ : Set V) : a✝.collinearTriple ↔ ∃ (u : V) (v : V) (w : V), sbtw u v w ∧ a✝ = {u, v, w}

inductive IsGenerated {V : Type u_1} [MetricSpace V] (s : Set V) : V → Prop

• basic {V : Type u_1} [MetricSpace V] {s : Set V} {x : V} : x ∈ s → IsGenerated s x
• extend_out {V : Type u_1} [MetricSpace V] {s : Set V} (u v w : V) : IsGenerated s u → IsGenerated s v → sbtw u v w → IsGenerated s w
• extend_in {V : Type u_1} [MetricSpace V] {s : Set V} (u v w : V) : IsGenerated s u → IsGenerated s v → sbtw u w v → IsGenerated s w

def GenerateLine {V : Type u_1} [MetricSpace V] (s : Set V) : Set V

Equations

• GenerateLine s = Set.ofPred (IsGenerated s)

theorem subset_generateLine {V : Type u_1} [MetricSpace V] (s : Set V) : s ⊆ GenerateLine s

theorem generateLine_close_right {V : Type u_1} [MetricSpace V] {s : Set V} {x y z : V} (hx : x ∈ GenerateLine s) (hy : y ∈ GenerateLine s) (h : sbtw x y z) : z ∈ GenerateLine s

theorem generateLine_close_left {V : Type u_1} [MetricSpace V] {s : Set V} {x y z : V} (hx : x ∈ GenerateLine s) (hy : y ∈ GenerateLine s) (h : sbtw z x y) : z ∈ GenerateLine s

theorem generateLine_close_middle {V : Type u_1} [MetricSpace V] {s : Set V} {x y z : V} (hx : x ∈ GenerateLine s) (hy : y ∈ GenerateLine s) (h : sbtw x z y) : z ∈ GenerateLine s

theorem generateLine_minimal {V : Type u_1} [MetricSpace V] {S L : Set V} (hL₀ : S ⊆ L) (out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L) (in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L) : GenerateLine S ⊆ L

def Line {V : Type u_1} [MetricSpace V] (a b : V) : Set V

Equations

• Line a b = GenerateLine {a, b}

@[simp]

theorem left_mem_Line {V : Type u_1} [MetricSpace V] {a b : V} : a ∈ Line a b

@[simp]

theorem right_mem_Line {V : Type u_1} [MetricSpace V] {a b : V} : b ∈ Line a b

theorem left_extend_mem_Line {V : Type u_1} [MetricSpace V] {a b c : V} (h : sbtw c a b) : c ∈ Line a b

theorem middle_extend_mem_Line {V : Type u_1} [MetricSpace V] {a b c : V} (h : sbtw a c b) : c ∈ Line a b

theorem right_extend_mem_Line {V : Type u_1} [MetricSpace V] {a b c : V} (h : sbtw a b c) : c ∈ Line a b

theorem Line_comm {V : Type u_1} [MetricSpace V] {u v : V} : Line u v = Line v u

def Set.IsLine {V : Type u_1} [MetricSpace V] (l : Set V) : Prop

Equations

• l.IsLine = ∃ (a : V) (b : V), a ≠ b ∧ Line a b = l

theorem Line_isLine {V : Type u_1} [MetricSpace V] {a b : V} (h : a ≠ b) : (Line a b).IsLine

theorem Set.IsLine.close_right {V : Type u_1} [MetricSpace V] {L : Set V} (hL : L.IsLine) {a b c : V} (ha : a ∈ L) (hb : b ∈ L) (hc : sbtw a b c) : c ∈ L

theorem Set.IsLine.close_left {V : Type u_1} [MetricSpace V] {L : Set V} (hL : L.IsLine) {a b c : V} (ha : a ∈ L) (hb : b ∈ L) (hc : sbtw c a b) : c ∈ L

theorem Set.IsLine.close_middle {V : Type u_1} [MetricSpace V] {L : Set V} (hL : L.IsLine) {a b c : V} (ha : a ∈ L) (hb : b ∈ L) (hc : sbtw a c b) : c ∈ L

theorem Set.IsLine.generateLine_subset {V : Type u_1} [MetricSpace V] {S L : Set V} (hL₀ : S ⊆ L) (hL : L.IsLine) : GenerateLine S ⊆ L

def NotCollinear {V : Type u_1} [MetricSpace V] (x y z : V) : Prop

Equations

• NotCollinear x y z = (x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l)

theorem notCollinear_iff {V : Type u_1} [MetricSpace V] {x y z : V} : NotCollinear x y z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l

theorem NotCollinear.rotate {V : Type u_1} [MetricSpace V] {u v w : V} (h : NotCollinear u v w) : NotCollinear v w u

theorem NotCollinear.swap {V : Type u_1} [MetricSpace V] {u v w : V} (h : NotCollinear u v w) : NotCollinear w v u

theorem exists_isLine {V : Type u_1} [MetricSpace V] [Nontrivial V] (a b : V) : ∃ (L : Set V), L.IsLine ∧ {a, b} ⊆ L

theorem NotCollinear.mk {V : Type u_1} [MetricSpace V] {x y z : V} [Nontrivial V] (hl : ∀ (l : Set V), l.IsLine → ¬{x, y, z} ⊆ l) : NotCollinear x y z

theorem thm_two {V : Type u_1} [MetricSpace V] [Nontrivial V] [Finite V] (h : ∀ (x y z : V), ¬NotCollinear x y z) : Set.univ.IsLine

theorem thm_two' {V : Type u_1} [MetricSpace V] [Nontrivial V] [Finite V] (h : ∀ (x y z : V), ¬NotCollinear x y z) : ∃ (l : Set V), l = Set.univ ∧ l.IsLine

def simpleEdges {V : Type u_1} [MetricSpace V] : SimpleGraph V

Equations

• simpleEdges = { Adj := fun (a b : V) => a ≠ b ∧ ∀ (x : V), ¬sbtw a x b, symm := ⋯, loopless := ⋯ }

@[simp]

theorem simpleEdges_adj {V : Type u_1} [MetricSpace V] (a b : V) : simpleEdges.Adj a b = (a ≠ b ∧ ∀ (x : V), ¬sbtw a x b)

def IsSimpleTriangle {V : Type u_1} [MetricSpace V] (x y z : V) : Prop

Equations

• IsSimpleTriangle x y z = (simpleEdges.Adj x y ∧ simpleEdges.Adj y z ∧ simpleEdges.Adj z x ∧ NotCollinear x y z)

theorem IsSimpleTriangle.swap {V : Type u_1} [MetricSpace V] {u v w : V} (h : IsSimpleTriangle u v w) : IsSimpleTriangle w v u

theorem one_implies_two {V : Type u_1} [MetricSpace V] [Finite V] (h : ∃ (x : V) (y : V) (z : V), NotCollinear x y z) : ∃ (x : V) (y : V) (z : V), IsSimpleTriangle x y z

def Delta {V : Type u_1} [MetricSpace V] (u v w : V) : ℝ

Equations

• Delta u v w = dist u v + dist v w - dist u w

theorem Delta_comm {V : Type u_1} [MetricSpace V] {u v w : V} : Delta u v w = Delta w v u

theorem Delta_pos_of {V : Type u_1} [MetricSpace V] {u v w : V} (h : NotCollinear u v w) : 0 < Delta u v w

theorem exists_third {V : Type u_1} [MetricSpace V] {a b : V} (hab : a ≠ b) (h : Line a b ≠ {a, b}) : ∃ c ∈ Line a b, sbtw c a b ∨ sbtw a c b ∨ sbtw a b c

theorem eqn_7 {V : Type u_1} [MetricSpace V] {a b c d : V} (habc : IsSimpleTriangle a b c) (habc_min : ∀ (a' b' c' : V), IsSimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') (hacd : sbtw a c d) (hcd : simpleEdges.Adj c d) : ¬simpleEdges.Adj b d

theorem eqn_8 {V : Type u_1} [MetricSpace V] {a b c d : V} (habc : IsSimpleTriangle a b c) (hacd : sbtw a c d) : dist a b + dist b d < dist a d + Delta a b c

def List.pathLength {V : Type u_1} [MetricSpace V] : List V → ℝ

Equations

• [].pathLength = 0
• [head].pathLength = 0
• (x_1 :: y :: xs).pathLength = dist x_1 y + (y :: xs).pathLength

theorem List.pathLength_nonneg {V : Type u_1} [MetricSpace V] (l : List V) : 0 ≤ l.pathLength

theorem List.pathLength_cons_le {V : Type u_1} [MetricSpace V] (x : V) {l : List V} : l.pathLength ≤ (x :: l).pathLength

theorem List.pathLength_triangle_left {V : Type u_1} [MetricSpace V] {v x : V} {l : List V} : (v :: l).pathLength ≤ dist v x + (x :: l).pathLength

theorem List.Sublist.pathLength_sublist {V : Type u_1} [MetricSpace V] {l₁ l₂ : List V} : l₁.Sublist l₂ → l₁.pathLength ≤ l₂.pathLength

def List.Special {V : Type u_1} [MetricSpace V] (a b d : V) : List V → Prop

Equations

• One or more equations did not get rendered due to their size.
• List.Special a b d [] = False
• List.Special a b d [head] = False
• List.Special a b d [head, head_1] = False

theorem List.Special.pathLength_le {V : Type u_1} [MetricSpace V] {a b d : V} {P : List V} : Special a b d P → P.pathLength ≤ [a, b, d].pathLength

theorem List.Special.chain_ne {V : Type u_1} [MetricSpace V] {a b d : V} {P : List V} : Special a b d P → IsChain (fun (x1 x2 : V) => x1 ≠ x2) P

theorem exists_min_dist (V : Type u_2) [MetricSpace V] [Finite V] : ∃ (r : ℝ), 0 < r ∧ ∀ (x y : V), x ≠ y → r ≤ dist x y

theorem length_mul_le_pathLength_add {V : Type u_1} [MetricSpace V] {r : ℝ} (hr : 0 ≤ r) (h : ∀ (x y : V), x ≠ y → r ≤ dist x y) {l : List V} : List.IsChain (fun (x1 x2 : V) => x1 ≠ x2) l → ↑l.length * r ≤ l.pathLength + r

theorem uniformly_bounded_of_chain_ne_of_pathLength_le (V : Type u_2) [MetricSpace V] [Finite V] (R : ℝ) : ∃ (n : ℕ), ∀ (l : List V), List.IsChain (fun (x1 x2 : V) => x1 ≠ x2) l → l.pathLength ≤ R → l.length ≤ n

theorem abd_special {V : Type u_1} [MetricSpace V] {a b c d : V} (habc : IsSimpleTriangle a b c) (hacd : sbtw a c d) (hbd' : b ≠ d) (hbd : ¬simpleEdges.Adj b d) : List.Special a b d [a, b, d]

theorem eqn_9 {V : Type u_1} [MetricSpace V] {a b c d : V} {P : List V} (habc : IsSimpleTriangle a b c) (hacd : sbtw a c d) (hbd' : b ≠ d) (hbd : ¬simpleEdges.Adj b d) (hP' : ∀ (P' : List V), List.Special a b d P' → P.pathLength ≤ P'.pathLength) : P.pathLength < dist a d + Delta a b c

theorem exists_simple_split_right {V : Type u_1} [MetricSpace V] [Finite V] {a b : V} (hab : a ≠ b) (hab' : ¬simpleEdges.Adj a b) : ∃ (c : V), sbtw a c b ∧ simpleEdges.Adj c b

theorem exists_simple_split_left {V : Type u_1} [MetricSpace V] [Finite V] {a b : V} (hab : a ≠ b) (hab' : ¬simpleEdges.Adj a b) : ∃ (c : V), sbtw a c b ∧ simpleEdges.Adj a c

theorem case1 {V : Type u_1} [MetricSpace V] [Finite V] [Nontrivial V] {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : IsSimpleTriangle a b c) (habc_min : ∀ (a' b' c' : V), IsSimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') (hacd : sbtw a c d) (hbd' : b ≠ d) (hbd : ¬simpleEdges.Adj b d) (hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength) (ha₁ : a₁ = a) (hα : NotCollinear a₁ a₂ a₃) (hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d) (hPc : List.IsChain (fun (x1 x2 : V) => x1 ≠ x2) (a₁ :: a₂ :: a₃ :: l)) (c₁1 : ¬simpleEdges.Adj a₁ a₂) (c₁2 : ¬simpleEdges.Adj a₂ a₃) : False

theorem case2 {V : Type u_1} [MetricSpace V] [Finite V] [Nontrivial V] {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : IsSimpleTriangle a b c) (habc_min : ∀ (a' b' c' : V), IsSimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') (hacd : sbtw a c d) (hbd' : b ≠ d) (hbd : ¬simpleEdges.Adj b d) (hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength) (ha₁ : a₁ = a) (hα : NotCollinear a₁ a₂ a₃) (hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d) (hPc : List.IsChain (fun (x1 x2 : V) => x1 ≠ x2) (a₁ :: a₂ :: a₃ :: l)) (c₁1 : simpleEdges.Adj a₁ a₂) (c₁2 : ¬simpleEdges.Adj a₂ a₃) : False

theorem case3 {V : Type u_1} [MetricSpace V] [Finite V] [Nontrivial V] {a b c d a₁ a₂ a₃ : V} {l : List V} (habc : IsSimpleTriangle a b c) (habc_min : ∀ (a' b' c' : V), IsSimpleTriangle a' b' c' → Delta a b c ≤ Delta a' b' c') (hacd : sbtw a c d) (hbd' : b ≠ d) (hbd : ¬simpleEdges.Adj b d) (hPmin : ∀ (P' : List V), List.Special a b d P' → (a₁ :: a₂ :: a₃ :: l).pathLength ≤ P'.pathLength) (ha₁ : a₁ = a) (hα : NotCollinear a₁ a₂ a₃) (hPd : (a₁ :: a₂ :: a₃ :: l).getLast ⋯ = d) (hPc : List.IsChain (fun (x1 x2 : V) => x1 ≠ x2) (a₁ :: a₂ :: a₃ :: l)) (c₁1 : ¬simpleEdges.Adj a₁ a₂) (c₁2 : simpleEdges.Adj a₂ a₃) : False

theorem two_implies_three {V : Type u_1} [MetricSpace V] [Finite V] [Nontrivial V] (h : ∃ (x : V) (y : V) (z : V), IsSimpleTriangle x y z) : ∃ (a : V) (b : V), a ≠ b ∧ Line a b = {a, b}

theorem sylvester_chvatal (V : Type u_2) [MetricSpace V] [Nontrivial V] [Finite V] : ∃ (a : V) (b : V), a ≠ b ∧ (Line a b = {a, b} ∨ Line a b = Set.univ)