chore(order/filter/at_top_bot): in order_top at_top = pure ⊤ (#3346)

Author: urkud

src/order/filter/at_top_bot.lean

@@ -68,6 +68,14 @@ lemma eventually_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop
   (∀ᶠ x in at_top, p x) ↔ (∃ a, ∀ b ≥ a, p b) :=
 by simp only [filter.eventually, filter.mem_at_top_sets, mem_set_of_eq]
 
+lemma order_top.at_top_eq (α) [order_top α] : (at_top : filter α) = pure ⊤ :=
+le_antisymm (le_pure_iff.2 $ mem_sets_of_superset (mem_at_top ⊤) $ λ b, top_unique)
+  (le_infi $ λ b, le_principal_iff.2 le_top)
+
+lemma tendsto_at_top_pure {α} [order_top α] (f : α → β) :
+  tendsto f at_top (pure $ f ⊤) :=
+(order_top.at_top_eq α).symm ▸ tendsto_pure_pure _ _
+
 @[nolint ge_or_gt]
 lemma eventually.exists_forall_of_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop}
   (h : ∀ᶠ x in at_top, p x) : ∃ a, ∀ b ≥ a, p b :=

src/topology/basic.lean

@@ -552,10 +552,11 @@ assume a s hs, mem_pure_sets.2 $ mem_of_nhds hs
 
 lemma tendsto_pure_nhds {α : Type*} [topological_space β] (f : α → β) (a : α) :
   tendsto f (pure a) (𝓝 (f a)) :=
-begin
-  rw [tendsto, filter.map_pure],
-  exact pure_le_nhds (f a)
-end
+tendsto_le_right (pure_le_nhds _) (tendsto_pure_pure f a)
+
+lemma order_top.tendsto_at_top {α : Type*} [order_top α] [topological_space β] (f : α → β) :
+  tendsto f at_top (𝓝 $ f ⊤) :=
+tendsto_le_right (pure_le_nhds _) $ tendsto_at_top_pure f
 
 @[simp] lemma nhds_ne_bot {a : α} : 𝓝 a ≠ ⊥ :=
 ne_bot_of_le_ne_bot pure_ne_bot (pure_le_nhds a)