gen_mem_nhds — Mathlib

English

If S ∈ 𝔖 and V ∈ 𝓤 β, then the set {g | ∀ x ∈ S, (f x, g x) ∈ V} belongs to 𝓝 f.

Русский

Если S ∈ 𝔖 и V ∈ 𝓤 β, то множество {g | ∀ x∈S, (f x, g x) ∈ V} принадлежит 𝓝 f.

LaTeX

$$$\{g : ∀ x ∈ S, (f x, g x) ∈ V\} \in 𝓝 f$ if S ∈ 𝔖 and V ∈ 𝓤 β.$$

Lean4

protected theorem gen_mem_nhds (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f :=
  by
  rw [UniformOnFun.nhds_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

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