case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ a = ((fun p => max p.fst p.snd) ∘ fun b => (a, b)) a
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ Tendsto (fun i => max a (f i)) l (𝓝 a)
convert ((continuous_max.comp (@Continuous.Prod.mk α α _ _ a)).tendsto a).comp h
no goals
case h.e'_5.h.e'_3
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderClosedTopology α
f g : β → α
l : Filter β
a : α
h : Tendsto f l (𝓝 a)
⊢ a = ((fun p => max p.fst p.snd) ∘ fun b => (a, b)) a
simp