gen_mem_uniformity — Mathlib

English

If S ∈ 𝔖 and V ∈ 𝓤 β, then UniformOnFun.gen 𝔖 S V belongs to the uniformity 𝓤 (α →ᵤ[𝔖] β).

Русский

Если S ∈ 𝔖 и V ∈ 𝓤 β, то UniformOnFun.gen 𝔖 S V принадлежит к равномерности 𝓤 (α →ᵤ[𝔖] β).

LaTeX

$$$\ UniformOnFun.gen 𝔖 S V ∈ 𝓤 (α →ᵤ[𝔖] β)$ if S ∈ 𝔖 and V ∈ 𝓤 β.$$

Lean4

protected theorem gen_mem_uniformity (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β) :=
  by
  rw [UniformOnFun.uniformity_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

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