α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abs (↑f j) < ε ∧ abs (↑g j) < ε
j : ℕ
ij : j ≥ i
H₁ : abs (↑f j) < ε
H₂ : abs (↑g j) < ε
⊢ abs (↑(f ⊓ g) j) < ε
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abs (↑f j) < ε ∧ abs (↑g j) < ε
j : ℕ
ij : j ≥ i
⊢ abs (↑(f ⊓ g) j) < ε
let ⟨H₁, H₂⟩ := H _ ij
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abs (↑f j) < ε ∧ abs (↑g j) < ε
j : ℕ
ij : j ≥ i
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abs (↑f j) < ε ∧ abs (↑g j) < ε
j : ℕ
ij : j ≥ i
H₁ : abs (↑f j) < ε
H₂ : abs (↑g j) < ε
⊢ abs (↑(f ⊓ g) j) < ε
rw [abs_lt] at H₁ H₂⊢
no goals
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : LimZero f
hg : LimZero g
ε : α
ε0 : ε > 0
i : ℕ
H : ∀ (j : ℕ), j ≥ i → abs (↑f j) < ε ∧ abs (↑g j) < ε
j : ℕ
ij : j ≥ i
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε
exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩