One positive bound for finitely many

Every "choose ε small enough for all of them" step in the development is this lemma: a finite family of positive bounds has a single positive bound below all of them. The polygonal-redrawing argument alone uses it three times, and the two-sided strip lemma chooses its vertex disks and edge blocks the same way.

It is stated for a predicate that is monotone downward in the bound rather than as a min fold, because no consumer wants the value — only that some positive value works for every member at once.

Blueprint

• exists_pos_le_of_finite — the numerical form.
• exists_pos_forall_of_finite — the form consumers use: a downward-monotone predicate holding at some positive bound for each member holds at one common positive bound.

theorem Schoenflies.exists_pos_le_of_finite {ι : Type u_1} {S : Set ι} (hS : S.Finite) {f : ι → ℝ} (hf : ∀ i ∈ S, 0 < f i) : ∃ ε > 0, ∀ i ∈ S, ε ≤ f i

A finite family of positive reals is bounded below by a positive real.

theorem Schoenflies.exists_pos_forall_of_finite {ι : Type u_1} {S : Set ι} (hS : S.Finite) {P : ι → ℝ → Prop} (hmono : ∀ (i : ι) ⦃δ ε : ℝ⦄, 0 < δ → δ ≤ ε → P i ε → P i δ) (hex : ∀ i ∈ S, ∃ ε > 0, P i ε) : ∃ ε > 0, ∀ i ∈ S, P i ε

The form the geometry uses: if a property that only gets easier as the bound shrinks holds at some positive bound for each member of a finite family, then it holds at one positive bound for all of them at once.