OAI/Analysis/SymmetricDomains/ContinuityPrinciple.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.point_isBoundedSymmetricDomain line 16
  2. theorem OAI.Release061.main_point line 25
  3. theorem OAI.Release061.bounded_cocompact_holomorphic_family_limit line 36
  4. theorem OAI.Release061.HolomorphicOnSubset.restrict line 59
  5. theorem OAI.Release061.HolomorphicOnSubset.locallyEventually line 66
  6. theorem OAI.Release061.continuity_principle_of_interior_anchor line 73
  7. theorem OAI.Release061.interior_anchor_of_boundary line 133
  8. theorem OAI.Release061.bounded_cocompact_continuity_principle line 149
  9. theorem OAI.Release061.bounded_cocompact_disc_continuity line 171
  10. def OAI.Release061.RelationSteps line 198
  11. theorem OAI.Release061.compact_relation_steps line 202
  12. theorem OAI.Release061.RelationSteps.refl line 225
  13. theorem OAI.Release061.RelationSteps.mono line 231