instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso

English

There is an instance stating that if P contains identities and respects isomorphisms, then the precoverage contains isomorphisms.

Русский

Существует экземпляр, утверждающий, что если P содержит тождества и сохраняет изоморфизмы, тогда предпокрытие содержит изоморфизмы.

LaTeX

$$instance [P.ContainsIdentities] [P.RespectsIso] : (precoverage P).HasIsos$$

Lean4

instance [P.ContainsIdentities] [P.RespectsIso] : (precoverage P).HasIsos := by dsimp only [precoverage]; infer_instance

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