OAI/Analysis/CircleDomains/Topology/BoundedRoundDisks.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded spherical round disks are Euclidean disks

The projective matrix action is converted to a norm inequality for its inverse. Excluding infinity makes the leading quadratic coefficient positive, so the completed-square formula gives a positive radius.

  1. theorem OAI.CircleDomainRigidity.mobius_smul_mem_unit_disk_iff line 20
  2. theorem OAI.CircleDomainRigidity.mobius_leading_normSq_pos line 39
  3. theorem OAI.CircleDomainRigidity.isRoundClosedDisk_eq_euclidean line 59
  4. theorem OAI.CircleDomainRigidity.isRoundClosedDisk_coe_closedBall line 92
  5. theorem OAI.CircleDomainRigidity.coe_closedBall_is_singleton_or_round line 103