OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumInflatedSeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Inflating a planar route family preserves its disjoint interiors.

  1. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_avoids_vertex line 9
  2. theorem OAI.ContinuumCoulomb.qmaInflatedPoint_disjoint line 20