OAI/Analysis/LipschitzHilbert/Trees/SourceAssignedModelInterval.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete covariant concentration input passes unchanged to the inhabited assigned model, retaining the original analyzing coefficient.

  1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.assignedInhabitedRawInterval_original line 29