OAI/Analysis/CircleDomains/Topology/JordanBoundaryBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bound on a Jordan boundary bounds its filled side.

  1. theorem OAI.CircleDomainRigidity.jordan_closure_subset_closedBall_of_frontier line 11