OAI/Analysis/Conductivity/Branching/RecoverJoinChild.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.recoverJoinChild line 12
2. lemma OAI.ScalarConductivity.div_self_div_eq line 16
3. lemma OAI.ScalarConductivity.recoverJoinChild_join line 21
4. lemma OAI.ScalarConductivity.coordinateJoin_recoverJoinChild line 30
5. lemma OAI.ScalarConductivity.continuousAt_recoverJoinChild line 39
6. lemma OAI.ScalarConductivity.coordinateJoin_zero line 56
7. lemma OAI.ScalarConductivity.coordinateJoin_one line 60
8. theorem OAI.ScalarConductivity.isOpen_finiteLaminate line 64
9. lemma OAI.ScalarConductivity.IsFiniteLaminate.permute line 86