Source indexedlemma · leanprover/lean4:v4.32.0

BKLNW.table_10_next_eq_of_adjacent

PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:66 to 76

Mathematical statement

Exact Lean statement

lemma table_10_next_eq_of_adjacent {x y : ℝ} (hxy : x < y) (hy : y ∈ table_10_bs)
    (hmin : ∀ z ∈ table_10_bs, x < z → y ≤ z) : table_10_next x = y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma table_10_next_eq_of_adjacent {x y : ℝ} (hxy : x < y) (hy : y ∈ table_10_bs)    (hmin : ∀ z ∈ table_10_bs, x < z → y ≤ z) : table_10_next x = y := by  have hne : (table_10_bs.filter (x < ·)).Nonempty :=    ⟨y, Finset.mem_filter.mpr ⟨hy, hxy⟩⟩  rw [table_10_next_eq_min' x hne]  apply le_antisymm  · exact Finset.min'_le _ y (Finset.mem_filter.mpr ⟨hy, hxy⟩)  · apply Finset.le_min'    intro z hz    obtain ⟨hz_mem, hz_gt⟩ := Finset.mem_filter.mp hz    exact hmin z hz_mem hz_gt