BohrSet.mem_chordSet_iff_nnnorm_width

lemma mem_chordSet_iff_nnnorm_width :    x ∈ B.chordSet ↔ ∀ ⦃ψ⦄, ψ ∈ B.frequencies → ‖1 - ψ x‖₊ ≤ B.width ψ := by  refine forall_congr' fun ψ => ?_  constructor  case mpr =>    intro h    rcases eq_top_or_lt_top (B.ewidth ψ) with h₁ | h₁    case inl => simp [h₁]    case inr =>      have : ψ ∈ B.frequencies := by simp [mem_frequencies, h₁]      specialize h this      rwa [←ENNReal.coe_le_coe, coe_width this] at h  case mp =>    intro h₁ h₂    rwa [←ENNReal.coe_le_coe, coe_width h₂]