OAI/Analysis/CircleDomains/Selection/RankedRealCodeLevels.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Real-coordinate generic levels with the inherited order on code labels.

  1. theorem OAI.CircleDomainRigidity.ranked_ae_code_real_level_singleton_on_tags line 16
  2. theorem OAI.CircleDomainRigidity.ranked_ae_code_real_band_tag_trace_null line 48
  3. theorem OAI.CircleDomainRigidity.ranked_ae_code_real_free_level_incidence_null line 138
  4. theorem OAI.CircleDomainRigidity.ranked_mean_code_real_level_intersections_finite line 203
  5. theorem OAI.CircleDomainRigidity.ranked_code_real_generic_levels line 312