OAI/Analysis/CircleDomains/Modulus/FiniteBandNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The distinct labels of physical terminals charge each original band at most once in the finite oscillation estimate.

  1. theorem OAI.CircleDomainRigidity.finite_label_band_norm_le line 13