OAI/Analysis/Conductivity/Sobolev/WeakCompactHilbert.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.continuous_weakDual_to_weakHilbert line 12
2. lemma OAI.ScalarConductivity.isCompact_weak_closedBall line 27
3. lemma OAI.ScalarConductivity.continuous_weak_pair line 48
4. lemma OAI.ScalarConductivity.isCompact_weak_product_closedBalls line 66
5. lemma OAI.ScalarConductivity.isCompact_weak_closure_of_pair_bounds line 82