OAI/Analysis/CircleDomains/Selection/LocalizedMeetingUnion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Splitting a meeting into its physical-domain and dust parts.

  1. theorem OAI.CircleDomainRigidity.localized_code_meeting_union_bound line 18