case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)

case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
⊢ Tendsto v l (𝓝 c)
by_cases h : c = 0
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : c = 0
⊢ Tendsto v l (𝓝 c)
subst c
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : u =o[l] fun _x => 1
⊢ v =o[l] fun _x => 1
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : Tendsto u l (𝓝 0)
⊢ Tendsto v l (𝓝 0)
rw [← isLittleO_one_iff ℝ] at hu⊢
no goals
case pos
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
huv : u ~[l] v
hu : u =o[l] fun _x => 1
⊢ v =o[l] fun _x => 1
simpa using (huv.symm.isLittleO.trans hu).add hu
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)
rw [← isEquivalent_const_iff_tendsto h] at hu⊢
no goals
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c
exact huv.symm.trans hu