uniformContinuous_sInf_rng — Mathlib

English

For f: α → β and u1 uniform on α, UniformContinuous[u1, sInf u2] f iff ∀ u ∈ u2, UniformContinuous[u1, u] f.

Русский

Для f: α → β и u1 на α, UniformContinuous[u1, sInf u2] f эквивалентно ∀ u ∈ u2, UniformContinuous[u1, u] f.

LaTeX

$$UniformContinuous[u1, sInf u2] f ↔ ∀ u ∈ u2, UniformContinuous[u1, u] f$$

Lean4

theorem uniformContinuous_sInf_rng {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)} :
    UniformContinuous[u₁, sInf u₂] f ↔ ∀ u ∈ u₂, UniformContinuous[u₁, u] f :=
  by
  delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]

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