instEssSurjCompObjPostOfFull — Mathlib

English

If F is essentially surjective, then (post F G S).EssSurj.

Русский

Если F является эссенциально сюръективной, то (post F G S) эссенциально сюръективен.

LaTeX

$$$ \forall F G S, [F.EssSurj] : (\mathrm{post}\ F\ G\ S).\mathrm{EssSurj}$. $$

Lean4

instance (F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Full] : (post F G S).EssSurj where
  mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩

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