Theorem: infinite_iff_arb_large (IIScExperiments/NumberTheory3.lean)

State before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
sorry
State after:
no goals