OAI/Geometry/PinnedDistances/ChartLimits.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Bounded.chart_probability line 15
2. lemma OAI.WeakPinned.Bounded.chart_map_comap line 25
3. lemma OAI.WeakPinned.Bounded.chart_ae_iff line 30
4. lemma OAI.WeakPinned.Bounded.weak_chart_closed line 37
5. lemma OAI.WeakPinned.Bounded.map_transport line 59
6. lemma OAI.WeakPinned.Bounded.map_pull_ac line 69
7. lemma OAI.WeakPinned.Bounded.map_full_range line 79
8. abbrev OAI.WeakPinned.Bounded.pairCoe line 85
9. abbrev OAI.WeakPinned.Bounded.quadCoe line 86
10. abbrev OAI.WeakPinned.Bounded.expandedCoe line 88
11. lemma OAI.WeakPinned.Bounded.pairCoe_open line 90
12. lemma OAI.WeakPinned.Bounded.quadCoe_open line 93
13. lemma OAI.WeakPinned.Bounded.expandedCoe_open line 96
14. lemma OAI.WeakPinned.Bounded.graph_edgeWeight_nonneg line 115
15. lemma OAI.WeakPinned.Bounded.graph_tripleWeight_nonneg line 120
16. def OAI.WeakPinned.Bounded.edgeProbability line 125
17. def OAI.WeakPinned.Bounded.expandedProbability line 131
18. lemma OAI.WeakPinned.Bounded.expandedProbability_edge line 137
19. lemma OAI.WeakPinned.Bounded.edgeProbability_dom₁ line 145
20. lemma OAI.WeakPinned.Bounded.edgeProbability_dom₂ line 157