strongEpi_map_of_isEquivalence — Mathlib

English

If F is an equivalence, then f is StrongEpi iff F.map f is StrongEpi.

Русский

Если F является эквивалентностью, то f — сильный эпиморфизм тогда и только тогда, когда F.map f — сильный эпиморфизм.

LaTeX

$$$$ \\operatorname{StrongEpi}(F.map f) \\iff \\operatorname{StrongEpi}(f). $$$$

Lean4

instance strongEpi_map_of_isEquivalence [F.IsEquivalence] (f : A ⟶ B) [_h : StrongEpi f] : StrongEpi (F.map f) :=
  F.asEquivalence.toAdjunction.strongEpi_map_of_strongEpi f

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