OAI/Analysis/CircleDomains/Selection/SubfamilyOverride.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Retain a prescribed real subfamily when choosing local branches.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.subfamilyOverride line 11
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.subfamilyOverride_at line 14
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.subfamilyOverride_of_notMem line 20