OAI/Analysis/CircleDomains/Transfer/ModelScalarDescent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A compact continuous target scalar constant on the actual omitted components yields a compact continuous scalar on the source sphere.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.scalar_constant_on_fibers line 18
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.compact_scalar_descent line 35