ClosedMapDescent.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A continuous scalar constant on each compact fiber descends through a closed quotient. Only continuity along the relevant fiber is needed.

theorem OAI.CircleDomainRigidity.closed_map_section_continuousAt_of_fiber line 12