`saturated_or_sub`

proved

show as: view math explainer →

module: IndisputableMonolith.Unification.RecognitionBandwidth
domain: Unification
line: 175 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Unification.RecognitionBandwidth on GitHub at line 175.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 172  demandedRate mass dynamicalTime < bandwidth area
 173
 174/-- Every system is either saturated or sub-saturated (excluded middle). -/
 175theorem saturated_or_sub (area mass dynamicalTime : ℝ) :
 176    IsSaturated area mass dynamicalTime ∨ IsSubSaturated area mass dynamicalTime := by
 177  unfold IsSaturated IsSubSaturated
 178  rcases le_or_lt (bandwidth area) (demandedRate mass dynamicalTime) with h | h
 179  · left; exact h
 180  · right; exact h
 181
 182end RecognitionBandwidth
 183end Unification
 184end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.