uniformContinuous_rangeFactorization_iff

English

Uniform continuity of the range factorization is equivalent to Uniform continuity of f.

Русский

Равномерно непрерывность разложения по образу эквивалентна равномерной непрерывности f.

LaTeX

$$$\text{UniformContinuous} (\text{rangeFactorization } f) \iff \text{UniformContinuous} f$$$

Lean4

@[simp]
theorem uniformContinuous_rangeFactorization_iff {f : α → β} :
    UniformContinuous (rangeFactorization f) ↔ UniformContinuous f :=
  (isUniformInducing_val _).uniformContinuous_iff

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