OAI/Analysis/CircleDomains/Topology/CompactMapContainment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact-open convergence retains containment of each fixed compact set in an open neighborhood of its limiting image.

  1. lemma OAI.CircleDomainRigidity.eventually_mapsTo_of_compact_convergence line 12