OAI/Analysis/StrictMeans/CompactFamily.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.StrictInverseFirstPower.locallyUniformLimit_zero_eventually line 19
  2. theorem OAI.StrictInverseFirstPower.locallyUniformLimit_injOn_or_constant line 76
  3. theorem OAI.StrictInverseFirstPower.locallyUniformLimit_injOn line 115
  4. abbrev OAI.StrictInverseFirstPower.UnitDisk line 136
  5. instance OAI.StrictInverseFirstPower.(instance at line 138) line 138
  6. def OAI.StrictInverseFirstPower.diskExtension line 140
  7. lemma OAI.StrictInverseFirstPower.diskExtension_coe line 144
  8. def OAI.StrictInverseFirstPower.DiskNormalized line 147
  9. abbrev OAI.StrictInverseFirstPower.DiskFamily line 152
  10. lemma OAI.StrictInverseFirstPower.diskExtension_tendsto line 154
  11. lemma OAI.StrictInverseFirstPower.disk_derivative_bound line 162
  12. lemma OAI.StrictInverseFirstPower.disk_lipschitz_bound line 173
  13. lemma OAI.StrictInverseFirstPower.disk_family_pointwise_bounded line 186
  14. lemma OAI.StrictInverseFirstPower.disk_family_equicontinuous line 195
  15. lemma OAI.StrictInverseFirstPower.isClosed_diskNormalized line 220
  16. lemma OAI.StrictInverseFirstPower.isCompact_diskNormalized line 240
  17. instance OAI.StrictInverseFirstPower.(instance at line 260) line 260
  18. instance OAI.StrictInverseFirstPower.(instance at line 262) line 262
  19. abbrev OAI.StrictInverseFirstPower.DiskHolomorphic line 274
  20. def OAI.StrictInverseFirstPower.diskDerivative line 277
  21. lemma OAI.StrictInverseFirstPower.continuous_diskDerivative line 282
  22. lemma OAI.StrictInverseFirstPower.continuous_diskDerivative_eval line 291
  23. lemma OAI.StrictInverseFirstPower.continuous_diskFamily_derivative line 295
  24. lemma OAI.StrictInverseFirstPower.diskFamily_derivative_ne_zero line 300