English
If the sequence seq hf U_mem tends to a, then f ⊆ nhds a.
Русский
Если последовательность seq hf U_mem сходится к a, то f ⊆ nhds a.
LaTeX
$$$\text{Tendsto}(\text{SequentiallyComplete.seq}(hf,U_{mem}),\mathbf{atTop}, \mathcal{N}(a)) \Rightarrow f \leq \mathcal{N}(a)$$$
Lean4
/-- If the sequence `SequentiallyComplete.seq` converges to `a`, then `f ≤ 𝓝 a`. -/
theorem le_nhds_of_seq_tendsto_nhds (U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) ⦃a : α⦄ (ha : Tendsto (seq hf U_mem) atTop (𝓝 a)) :
f ≤ 𝓝 a :=
le_nhds_of_cauchy_adhp_aux
(fun s hs => by
rcases U_le s hs with ⟨m, hm⟩
rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩
refine ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_, seq_mem hf U_mem _⟩
· have := le_max_left m n
exact Set.Subset.trans (setSeq_prod_subset hf U_mem this this) hm
· exact hm (hn _ <| le_max_right m n))
