BKLNW_app.table_8_ε_le_of_row

lemma table_8_ε_le_of_row {b b₀ ε : ℝ} (hmem : (b₀, ε) ∈ table_8) (hb : b₀ ≤ b) :    table_8_ε b ≤ ε := by  classical  let S : Set ℝ := { ε | ∃ p ∈ table_8, p.1 ≤ b ∧ p.2 = ε }  have hmemS : ε ∈ S := by    exact ⟨(b₀, ε), hmem, hb, rfl⟩  have hfinite : S.Finite := by    refine (Set.Finite.subset (s := { ε | ε ∈ table_8.map Prod.snd }) ?_ ?_)    · simpa using (List.finite_toSet (table_8.map Prod.snd))    · intro ε hε      rcases hε with ⟨p, hp, _, rfl⟩      have hp' : p.2 ∈ table_8.map Prod.snd := by        exact (List.mem_map).2 ⟨p, hp, rfl⟩      simpa using hp'  have hbdd : BddBelow S := hfinite.bddBelow  simpa [table_8_ε, S] using (csInf_le hbdd hmemS)