OAI/Analysis/CircleDomains/Sobolev/SobolevNullFibers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The graph-null theorem removes exceptional scalar fibers for the actual continuous local Sobolev representative.

  1. lemma OAI.CircleDomainRigidity.physical_graph_null_fibers line 13
  2. lemma OAI.CircleDomainRigidity.locally_sobolev_null_fibers line 44