Registry · Proposition II.P04 established formalized

II.P04 — Cylinders Are Balls

Stage-k cylinders equal both closed and open ultrametric balls, so cylinders and balls are identical objects in the cylinder topology.

Book II Part 2 Ch. 10

Dependency Graph

Depends on (2)

II.D10 II.D13

Lean Formalization

Module: TauLib.BookII.Domains.Ultrametric

Symbol: cyl_eq_ball_check