Registry · Theorem II.T15 established formalized

II.T15 — Betweenness Axioms

The betweenness relation from the ultrametric distance satisfies all three Tarski betweenness axioms (identity, transitivity, connectivity).

Book II Part 4 Ch. 18

Dependency Graph

Depends on (2)

II.D19 II.D13

Depended on by (8)

II.D71 II.R07 II.T17 II.T18 II.T19 II.T45 II.D91 II.D92

Lean Formalization

Module: TauLib.BookII.Geometry.Betweenness

Symbol: between_identity_check