OAI/Analysis/LipschitzHilbert/Trees/SourceShiftedReferenceVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The deterministic residual collection of an actual shifted source path lies in its short reference cone. Its reference good event therefore controls the original physical prefix used by every active unary segment.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.shifted_residual_referenceCondition line 17
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.shifted_residual_reference_variation line 39