OAI/Analysis/CircleDomains/Sobolev/LineDerivativeLocality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Classical one-dimensional derivatives are local on arbitrary level sets, outside the countable set of one-sided isolated points.

  1. lemma OAI.CircleDomainRigidity.ae_deriv_zero_of_eqOn_const line 15
  2. lemma OAI.CircleDomainRigidity.ae_derivative_eq_of_eqOn line 29