OAI/Analysis/CircleDomains/Transfer/CountableRealTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Countably many real tests and mandatory marked ends

Every finite prefix is transferred by the actual assembled construction. An increasing sequence of finite mandatory sets puts each fixed mark in all sufficiently late models. Prescribed neighborhoods and source cores are retained at each stage.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates line 23
  2. def OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.NaturalCompatibility line 49
  3. abbrev OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.Stage line 57
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.nonempty_stage line 63
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_countable_real_transfer line 89