OAI/Analysis/LipschitzHilbert/Trees/SourceReferenceWeightedMaximal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weighted long-tree control in the original physical coordinates. The reference cone is an actual restriction of the original labels.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_reference_weighted_tree_maximal line 17