le_nhds_iff_forall_dual_apply_le_nhds

English

For l a filter and A: E →WOT F, l ≤ nhds A if and only if for every x ∈ E and every continuous functional y on F, the pushforward of l under T ↦ y(Tx) is ≤ nhds (y(Ax)).

Русский

Для фильтра l и A: E →WOT F выполняется равенство l ≤ nhds A тогда и только тогда, когда для каждого x ∈ E и каждого непрерывного функционала y на F, образ фильтра l через T ↦ y(Tx) удовлетворяет неравенству ≤ nhds (y(Ax)).

LaTeX

$$$l \le \mathcal{N} A \iff \\forall x \\in E, \\forall y \\in F^*, \\ \\mathrm{map} (T \\mapsto y(Tx))\, l \\le \\mathcal{N} (y(Ax)).$$$

Lean4

theorem le_nhds_iff_forall_dual_apply_le_nhds {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} :
    l ≤ 𝓝 A ↔ ∀ x (y : F⋆), l.map (fun T => y (T x)) ≤ 𝓝 (y (A x)) :=
  tendsto_iff_forall_dual_apply_tendsto (f := id)

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