tendsto_nhds_true — Mathlib

English

A function tends to True in the nhds True sense if and only if p(x) holds for eventually all x in the filter l.

Русский

Функция стремится к True в смысле nhds True тогда и только тогда, когда свойство p(x) выполняется почти для всех x по фильтру l.

LaTeX

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

Lean4

theorem tendsto_nhds_true {l : Filter α} {p : α → Prop} : Tendsto p l (𝓝 True) ↔ ∀ᶠ x in l, p x := by simp

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