OAI/Analysis/CircleDomains/Selection/FiniteJumpFloor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finitely many positive old tolls and the positive new-jump floor have one common positive real lower bound.

  1. theorem OAI.CircleDomainRigidity.exists_common_positive_jump_floor line 13