isUniformInducing_rangeFactorization_iff

English

IsUniformInducing (rangeFactorization f) iff IsUniformInducing f.

Русский

IsUniformInducing (rangeFactorization f) эквивалентно IsUniformInducing f.

LaTeX

$$$\IsUniformInducing(\operatorname{rangeFactorization} f) \iff \IsUniformInducing f$$$

Lean4

@[simp]
theorem isUniformInducing_rangeFactorization_iff {f : α → β} :
    IsUniformInducing (rangeFactorization f) ↔ IsUniformInducing f :=
  (isUniformInducing_val (range f)).isUniformInducing_comp_iff.symm

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