Registry · Theorem II.T05 established formalized

II.T05 — Ultrametric Triangle Inequality

Ultrametric Triangle Inequality

Book II Part 2 Ch. 10

Dependency Graph

Depends on (2)

II.D13 II.D12

Depended on by (3)

II.D19 II.R05 II.T08

Lean Formalization

Module: TauLib.BookII.Domains.Ultrametric

Symbol: triangle_check