Theorem: mem_atInf_iff (Ray/Misc/AtInf.lean)

State before:
X : Type
inst✝ : Norm X
s : Set X
⊢ s ∈ atInf ↔ ∃ r, {x | ‖x‖ > r} ⊆ s
Tactic:
simp only [Filter.hasBasis_iff.mp atInf_basis s, exists_true_left, true_and]
State after:
no goals