OAI/Analysis/CircleDomains/Probability/CenteredSubtypeLaw.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The compact terminal-arc law supplies the actual supported law and compact disk-arc image used by the mean stream construction.

  1. theorem OAI.CircleDomainRigidity.exists_centered_subtype_arc_law line 19