OAI/Analysis/Conductivity/Variational/CompactFiberDecomposition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.compactFiberMarginal line 15
2. lemma OAI.ScalarConductivity.compactFiberMarginal_smooth line 18
3. lemma OAI.ScalarConductivity.compactFiberMarginal_support line 28
4. lemma OAI.ScalarConductivity.exists_unit_interval_bump line 43
5. theorem OAI.ScalarConductivity.compact_fiber_decomposition line 78
6. lemma OAI.ScalarConductivity.smooth_unit_interval_trace line 136
7. theorem OAI.ScalarConductivity.smooth_unit_face_trace line 174