surjective_fromQuotient_iff_surjective_π

English

Surjectivity of the quotient-from-solution map is equivalent to surjectivity of π.

Русский

Существенность отображения fromQuotient равна существенности π.

LaTeX

$$$\text{Surjective}(\text{solution.fromQuotient}) \; \iff \; \text{Surjective}(\text{solution.π})$$$

Lean4

theorem surjective_fromQuotient_iff_surjective_π :
    Function.Surjective solution.fromQuotient ↔ Function.Surjective solution.π := by
  simpa only [← fromQuotient_comp_toQuotient] using
    (Function.Surjective.of_comp_iff (f := solution.fromQuotient) relations.surjective_toQuotient).symm

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