OAI/Analysis/CircleDomains/Topology/MixedMapDiskExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual assigned mixed limit avoids every retained source test in the map--disk topology used for countable selection.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedMixedModelLimit.not_mem_mapDiskExclusion line 13