OAI/Analysis/SymmetricDomains/QuadraticDomainConnectedComponent.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.semialgebraic_boundary_fiber_closure line 37
  2. def OAI.Release061.quadraticDomain line 80
  3. def OAI.Release061.quadraticDomainCoordinates line 83
  4. lemma OAI.Release061.quadraticDomain_eq_preimage line 117
  5. theorem OAI.Release061.quadraticDomain_isOpen line 125
  6. theorem OAI.Release061.quadraticDomain_isConnected line 131
  7. lemma OAI.Release061.quadraticDomain_axis line 138
  8. lemma OAI.Release061.quadraticDomain_translation line 144
  9. lemma OAI.Release061.quadraticDomain_unit_rotation line 149
  10. lemma OAI.Release061.quadraticDomain_positive_dilation line 154
  11. theorem OAI.Release061.quadraticDomain_connectedComponent line 169