OAI/Analysis/MassAction/CompactBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.compact_positive_uniform_bounds line 13

   Source documentation

   A compact set in a finite-dimensional positive orthant lies in a uniform positive box. Neither nonemptiness nor positive dimension is necessary.

   theorem compact_positive_uniform_bounds {ι : Type uIota} [Finite ι]
       {K : Set (ι → ℝ)} (hK : IsCompact K)
       (hpos : ∀ x ∈ K, ∀ i, 0 < x i) :
       ∃ ε : ℝ, 0 < ε ∧ ε < 1 ∧
         ∀ x ∈ K, ∀ i, ε ≤ x i ∧ x i ≤ ε⁻¹ := by
   …