OAI/Analysis/CircleDomains/Selection/FullSelectedCompatibility.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compatibility against the whole ordered selected family implies admissibility for the same greedy open selection.

  1. theorem OAI.CircleDomainRigidity.seed_and_selected_subset_ordered_range line 15
  2. theorem OAI.CircleDomainRigidity.seeded_allowed_of_ordered_compatible line 28