Theorem: LoVe.CauchySeq.Setoid_iff (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
f g : CauchySeq
⊢ f ≈ g ↔ ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf f m - seqOf g m| < ε
Tactic:
rfl
State after:
no goals