continuous_rangeFactorization_iff

English

If f: X → Y is continuous, then the induced range factorization map is continuous.

Русский

Если f: X → Y непрерывно, то соответствующее разложение по диапазону непрерывно.

LaTeX

$$$\text{Continuous}(f) \Rightarrow \text{Continuous}(\text{rangeFactorization } f).$$$

Lean4

@[simp]
theorem continuous_rangeFactorization_iff {f : X → Y} : Continuous (rangeFactorization f) ↔ Continuous f :=
  IsInducing.subtypeVal.continuous_iff

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