Registry · Theorem II.T16 established formalized

II.T16 — Congruence Axioms

The ultrametric congruence relation satisfies all six Tarski congruence axioms (reflexivity, identity, transitivity, segment construction, five-segment, inner transitivity).

Book II Part 4 Ch. 19

Dependency Graph

Depends on (2)

II.D20 II.D13

Depended on by (3)

II.D71 II.T19 II.T45

Lean Formalization

Module: TauLib.BookII.Geometry.Congruence

Symbol: congruence_reflexive_check