uniformContinuous_sInf_dom — Mathlib

English

If u1 is in u1-set and f: α → β is uniformly continuous from u to u2, then UniformContinuous[sInf u1, u2] f.

Русский

Если u принадлежит множеству u1, и f равномерно непрерывна от u к u2, то UniformContinuous[sInf u1, u2] f.

LaTeX

$$UniformContinuous[sInf u1, u2] f$$

Lean4

theorem uniformContinuous_sInf_dom {f : α → β} {u₁ : Set (UniformSpace α)} {u₂ : UniformSpace β} {u : UniformSpace α}
    (h₁ : u ∈ u₁) (hf : UniformContinuous[u, u₂] f) : UniformContinuous[sInf u₁, u₂] f :=
  by
  delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity]
  exact tendsto_iInf' ⟨u, h₁⟩ hf

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