CencovPetz.RationalDensity

Density of common-denominator (“rational”) points in the finite open simplex.

This is the final topological input for the finite Čencov/Chentsov argument: once the metric identity is proved on the dense family of rational points, continuity hypotheses extend it to all simplex points.

Main result

• CencovPetz.Simplex.dense_setOf_isRational

theorem LeanPool.CencovPetz.Simplex.dense_setOf_isRational {α : Type u_1} [Fintype α] [Nonempty α] : Dense {p : Simplex α | p.IsRational}