OAI/Analysis/Conductivity/Variational/SmoothCompactExtension.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.exists_smooth_compact_extension line 24
2. lemma OAI.ScalarConductivity.derivative_test_integral_congr line 60
3. theorem OAI.ScalarConductivity.local_compact_piola_Cauchy_difference line 72
4. lemma OAI.ScalarConductivity.null_frontier_union line 118
5. lemma OAI.ScalarConductivity.null_frontier_biUnion_finset line 127
6. lemma OAI.ScalarConductivity.openDisjointify_null_frontier line 138
7. theorem OAI.ScalarConductivity.finite_disjoint_localization_null line 150