OAI/Analysis/Conductivity/Variational/RankProjectionFirst.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.TwoFieldRankRegular.projectFirst line 11
2. lemma OAI.ScalarConductivity.RegularPatch.projectFirst line 46
3. lemma OAI.ScalarConductivity.mem_regularRegion_projectFirst line 57
4. lemma OAI.ScalarConductivity.fderiv_projectFirst line 72
5. def OAI.ScalarConductivity.WeakFiniteTensorPair.projectFirst line 91
6. lemma OAI.ScalarConductivity.linearTensorPullback_refl line 140
7. def OAI.ScalarConductivity.WeakFiniteTensorPair.output line 149
8. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.output_v line 153
9. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.output_E line 159
10. def OAI.ScalarConductivity.scaleSecondEquiv line 168
11. lemma OAI.ScalarConductivity.scaleSecondEquiv_apply line 173