Theorem: tendsto_zero_of_forall_abs_le (ForML/Dirac.lean)

State before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
⊢ Tendsto f atTop (nhds 0)
Tactic:
simp [Metric.tendsto_atTop]
State after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |f n| < ε

State before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
intro ε hε
State after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε

State before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
simp [Metric.tendsto_atTop] at h
State after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε

State before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
specialize h ε hε
State after:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε

State before:
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
h : ∃ N, ∀ (n : α), N ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
rcases h with ⟨a, ha⟩
State after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε

State before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
Tactic:
exists a
State after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∀ (n : α), a ≤ n → |f n| < ε

State before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
⊢ ∀ (n : α), a ≤ n → |f n| < ε
Tactic:
intro x hx
State after:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
x : α
hx : a ≤ x
⊢ |f x| < ε

State before:
case intro
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
ε : ℝ
hε : 0 < ε
a : α
ha : ∀ (n : α), a ≤ n → |g n| < ε
x : α
hx : a ≤ x
⊢ |f x| < ε
Tactic:
exact lt_of_le_of_lt (hfg x) (lt_of_abs_lt (ha x hx))
State after:
no goals