OAI/Analysis/LipschitzHilbert/Packets/PacketDataAssignedModelInterval.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.PacketLatticeData.assignedInhabitedRawInterval_original line 29