OAI/NumberTheory/Jacobsthal/Partitions/FiberCardinalityConstancy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosGlobalFiberBranches.orderIsoOfNatCardEq line 13
  2. theorem OAI.Erdos970.ErdosGlobalFiberBranches.finite_orderIso_unique line 20
  3. def OAI.Erdos970.ErdosGlobalFiberBranches.orderIsoOfStrictMonoSurjective line 23
  4. theorem OAI.Erdos970.ErdosGlobalFiberBranches.orderIsoOfStrictMonoSurjective_apply line 28
  5. structure OAI.Erdos970.ErdosLocalFiberGraphs.FiberCharts line 44
  6. theorem OAI.Erdos970.ErdosLocalFiberGraphs.exists_bounded_fiber_charts line 64
  7. def OAI.Erdos970.ErdosGlobalFiberBranches.chartOrderIso line 146
  8. theorem OAI.Erdos970.ErdosGlobalFiberBranches.chartOrderIso_val line 158
  9. theorem OAI.Erdos970.ErdosLocalFiberGraphs.boundedFiber_card_le_degree line 173
  10. theorem OAI.Erdos970.ErdosLocalFiberGraphs.FiberCharts.fiber_finite line 194
  11. theorem OAI.Erdos970.ErdosLocalFiberGraphs.FiberCharts.fiber_card_eq line 200
  12. theorem OAI.Erdos970.ErdosLocalFiberGraphs.FiberCharts.unique_root_in_tube line 205
  13. theorem OAI.Erdos970.ErdosLocalFiberGraphs.FiberCharts.all_roots_regular line 212
  14. theorem OAI.Erdos970.ErdosLocalFiberGraphs.locally_constant_fiber_card line 220
  15. def OAI.Erdos970.ErdosLocalFiberGraphs.regularParameters line 240
  16. theorem OAI.Erdos970.ErdosLocalFiberGraphs.continuous_horizontal_eval line 244
  17. theorem OAI.Erdos970.ErdosLocalFiberGraphs.regularParameters_isOpen line 249
  18. theorem OAI.Erdos970.ErdosLocalFiberGraphs.fiber_card_eventually_eq line 259
  19. theorem OAI.Erdos970.ErdosGlobalFiberBranches.continuousOn_fiber_card line 277
  20. theorem OAI.Erdos970.ErdosGlobalFiberBranches.fiber_card_eq_on_preconnected line 287