instContainsIdentitiesScheme — Mathlib

English

If W and P are morphism properties that contain identities, then the source-local-closure of W along P also contains identities.

Русский

Если W и P — свойства морфизмов, содержащие тождества, то источник-локальное замыкание sourceLocalClosure W P также содержит тождественные морфизмы.

LaTeX

$$$ (W.ContainIdentities) \land (P.ContainIdentities) \Rightarrow (sourceLocalClosure\ W\ P).ContainsIdentities $$$

Lean4

instance [W.ContainsIdentities] [P.ContainsIdentities] : (sourceLocalClosure W P).ContainsIdentities :=
  ⟨fun X ↦ ⟨X.coverOfIsIso (𝟙 X), fun _ ↦ P.id_mem _⟩⟩

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