uniformContinuous_iInf_dom — Mathlib

English

If hf: UniformContinuous[u1, u2] f for an index i, then UniformContinuous[iInf u1, u2] f.

Русский

Если для некоторого индекса i верно UniformContinuous[u1, u2] f, то UniformContinuous[iInf u1, u2] f.

LaTeX

$$UniformContinuous f → UniformContinuous[iInf u1, u2] f$$

Lean4

theorem uniformContinuous_iInf_dom {f : α → β} {u₁ : ι → UniformSpace α} {u₂ : UniformSpace β} {i : ι}
    (hf : UniformContinuous[u₁ i, u₂] f) : UniformContinuous[iInf u₁, u₂] f :=
  by
  delta UniformContinuous
  rw [iInf_uniformity]
  exact tendsto_iInf' i hf

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