OAI/Analysis/Conductivity/Geometry/RegularPatch.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.TwoFieldRankRegular.congr line 23
2. def OAI.ScalarConductivity.RegularPatch line 36
3. lemma OAI.ScalarConductivity.RegularPatch.mono line 41
4. lemma OAI.ScalarConductivity.RegularPatch.congr line 46
5. def OAI.ScalarConductivity.regularRegion line 52
6. lemma OAI.ScalarConductivity.isOpen_regularRegion line 56
7. lemma OAI.ScalarConductivity.regularRegion_subset line 60
8. lemma OAI.ScalarConductivity.mem_regularRegion_iff line 68
9. lemma OAI.ScalarConductivity.exists_precompact_regular_patch line 73