OAI/Analysis/CircleDomains/Topology/ClosedRelationIntermediateValue.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A closed compact-valued relation with connected fibers has the intermediate-value property over a connected source. This is the interval coverage needed for the finite-hole slice estimate.

  1. theorem OAI.CircleDomainRigidity.closed_relation_intermediate_value line 15