essSurjInducedFunctor — Mathlib

English

If e: C' ≃ D is an equivalence, then the induced functor inducedFunctor e is essentially surjective.

Русский

Если e: C' ≃ D — эквивалентность, то индуцированная функторная функция inducedFunctor e обладает свойством essSurj.

LaTeX

$$InducedFunctor e .EssSurj$$

Lean4

instance essSurjInducedFunctor {C' : Type*} (e : C' ≃ D) : (inducedFunctor e).EssSurj where
  mem_essImage Y := ⟨e.symm Y, by simpa using ⟨default⟩⟩

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