TODO

Axiomatic betweenness

@[implicit_reducible]

def MetricSBtw {V : Type u_1} [MetricSpace V] : SBtw V

Equations

• MetricSBtw = { sbtw := fun (u v w : V) => u ≠ v ∧ u ≠ w ∧ v ≠ w ∧ dist u v + dist v w = dist u w }

theorem MetricSpace.sbtw_iff {V : Type u_1} [MetricSpace V] {u v w : V} : sbtw u v w ↔ u ≠ v ∧ u ≠ w ∧ v ≠ w ∧ dist u v + dist v w = dist u w

theorem SBtw.sbtw.ne12 {V : Type u_1} [MetricSpace V] {u v w : V} (h : sbtw u v w) : u ≠ v

theorem SBtw.sbtw.ne13 {V : Type u_1} [MetricSpace V] {u v w : V} (h : sbtw u v w) : u ≠ w

theorem SBtw.sbtw.ne23 {V : Type u_1} [MetricSpace V] {u v w : V} (h : sbtw u v w) : v ≠ w

theorem SBtw.sbtw.dist {V : Type u_1} [MetricSpace V] {u v w : V} (h : sbtw u v w) : Dist.dist u v + Dist.dist v w = Dist.dist u w

theorem SBtw.sbtw.symm {V : Type u_1} [MetricSpace V] {u v w : V} : sbtw u v w → sbtw w v u

theorem SBtw.comm {V : Type u_1} [MetricSpace V] {u v w : V} : sbtw u v w ↔ sbtw w v u

theorem sbtw_iff_of_ne {V : Type u_1} [MetricSpace V] {u v w : V} (h12 : u ≠ v) (h13 : u ≠ w) (h23 : v ≠ w) : sbtw u v w ↔ dist u v + dist v w = dist u w

theorem sbtw_mk {V : Type u_1} [MetricSpace V] {u v w : V} (h12 : u ≠ v) (h23 : v ≠ w) (h : dist u v + dist v w ≤ dist u w) : sbtw u v w

theorem SBtw.sbtw.right_cancel {V : Type u_1} [MetricSpace V] {u v w x : V} (h : sbtw u v x) (h' : sbtw v w x) : sbtw u v w

theorem SBtw.sbtw.asymm_right {V : Type u_1} [MetricSpace V] {u v x : V} (h : sbtw u v x) (h' : sbtw v u x) : False

theorem SBtw.sbtw.trans_right' {V : Type u_1} [MetricSpace V] {u v w x : V} (h : sbtw u v x) (h' : sbtw v w x) : sbtw u w x