OAI/Analysis/CircleDomains/Selection/MappedGenericLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing the level-first estimates between a coded probability law, its actual path law, and a supported subtype law.

  1. theorem OAI.CircleDomainRigidity.map_generic_levels line 18
  2. theorem OAI.CircleDomainRigidity.supportedProbability_generic_levels line 73