CompactContinuation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem326.exists_global_massAction_of_compact_trapping line 13
theorem OAI.Problem326.isForwardInvariant_of_compact_trapping line 29
theorem OAI.Problem326.massAction_isForwardInvariant_of_compact_trapping line 43
Source documentation
No extra regularity hypothesis is necessary for the polynomial mass-action field: compact trapping of finite solutions implies full forward invariance.
```
theorem massAction_isForwardInvariant_of_compact_trapping
    {d : ℕ} {N : ReactionNetwork d} {κ : Reaction N → ℝ}
    {K : Set (Fin d → ℝ)} (hK : IsCompact K)
    (htrap : ∀ z ∈ K, ∀ (T : ℝ) (x : ℝ → (Fin d → ℝ)),
      0 ≤ T → IsForwardSolutionOn N κ z T x →
      ∀ t ∈ Icc (0 : ℝ) T, x t ∈ K) :
    IsForwardInvariant N κ K :=
…
```
Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.IsForwardSolutionOn, OAI.Problem326.IsForwardInvariant