def
definition
IsSubSaturated
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.RecognitionBandwidth on GitHub at line 171.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
168 demandedRate mass dynamicalTime ≥ bandwidth area
169
170/-- A system is **sub-saturated** (Newtonian regime) when demand < bandwidth. -/
171def IsSubSaturated (area mass dynamicalTime : ℝ) : Prop :=
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