OAI/Analysis/LipschitzHilbert/Packets/SourceSupportedInhabitedGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing empty labels preserves packetwise top geometry.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.inhabitedFamily_supportedTopGeometry line 12