uniformEquicontinuous_iInf_rng — Mathlib

English

UniformEquicontinuous F is equivalent to ∀ k, UniformEquicontinuous (F) under iInf decomposition.

Русский

Униформная эконтинуированность через iInf разложение по компонентам.

LaTeX

$$$\\operatorname{UniformEquicontinuous} F \\iff \\forall k, \\operatorname{UniformEquicontinuous} F.$$$

Lean4

theorem uniformEquicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} :
    UniformEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, UniformEquicontinuous (uα := u k) F :=
  by
  simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)]
  rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng]

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