OAI/Analysis/AncientFlat/Weighted/WeightedCharts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FlatWeighted.sigma_pos line 11
2. lemma OAI.FlatWeighted.chart_zero line 16
3. lemma OAI.FlatWeighted.zero_localDomain line 17
4. lemma OAI.FlatWeighted.continuous_chart line 21
5. lemma OAI.FlatWeighted.isOpen_localDomain line 25
6. lemma OAI.FlatWeighted.YBound.pointwise line 32
7. def OAI.FlatWeighted.unchart line 40
8. lemma OAI.FlatWeighted.continuous_unchart line 43
9. lemma OAI.FlatWeighted.unchart_self line 45
10. lemma OAI.FlatWeighted.chart_unchart line 47
11. lemma OAI.FlatWeighted.YBound.continuousOn line 50