OAI/Geometry/PinnedDistances/ProductLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.weak_product_limit line 20
2. lemma OAI.WeakPinned.Bounded.weak_pair_product_limit line 55
3. lemma OAI.WeakPinned.Bounded.pair_of_pi_map line 76
4. lemma OAI.WeakPinned.Bounded.weak_double_product_limit line 111
5. lemma OAI.WeakPinned.Bounded.measure_le_of_continuous_lintegral line 154
6. lemma OAI.WeakPinned.Bounded.weak_domination line 166
7. lemma OAI.WeakPinned.Bounded.weak_map_eq line 194
8. lemma OAI.WeakPinned.Bounded.weak_map_domination line 205