tendsto_nhds_generateFrom_iff — Mathlib

English

A map m from α to β tends to nhds b in the generateFrom topology iff for every s in g with b ∈ s, m^{-1}(s) ∈ f.

Русский

Отображение m между пространствами α и β сходится к окрестностям b в топологии generateFrom тогда и только тогда, когда для каждого множества s из g, в котором b ∈ s, прообраз m^{-1}(s) принадлежит фильтру f.

LaTeX

$$$\\mathrm{Tendsto}\, m\\ f\\ (\\mathrm{nhds}\\ b) \\iff \\forall s \\in g,\\; b \\in s \\Rightarrow m^{-1}(s) \\in f.$$$

Lean4

theorem tendsto_nhds_generateFrom_iff {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β} :
    Tendsto m f (@nhds β (generateFrom g) b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f := by
  simp only [nhds_generateFrom, @forall_swap (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp, tendsto_principal]; rfl

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