OAI/Analysis/CircleDomains/Selection/AllowedCountableConcatenation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A continuous concatenation of countably many allowed paths is allowed when its remaining parameter times are countable and its physical length is finite. All tags and incidence estimates are constructed explicitly.

  1. theorem OAI.CircleDomainRigidity.allowedTaggedPath_concatenated line 22
  2. theorem OAI.CircleDomainRigidity.exists_allowed_countable_concatenation line 47