tendsto_nhds_Prop — Mathlib

English

For any p: α → Prop and q ∈ Prop, Tendsto p l (nhds q) holds iff q implies p(x) eventually along l.

Русский

Для p: α → Prop и q ∈ Prop, сходимость p к nhds q по l эквивалентна тому, что q влечет Eventually p(x) вдоль l.

LaTeX

$$$\\text{Tendsto } p\\ l\\ (\\mathcal{N}(q)) \\iff (q \\to \\forall^\\text{F} x \\in l,\\; p(x)).$$$

Lean4

theorem tendsto_nhds_Prop {l : Filter α} {p : α → Prop} {q : Prop} : Tendsto p l (𝓝 q) ↔ (q → ∀ᶠ x in l, p x) := by
  by_cases q <;> simp [*]

Похожие утверждения