containsIdentities — Mathlib

English

If every W_j contains identities, then the pi construction over W contains identities.

Русский

Если для каждого j свойство W_j содержит идентичности, то свойство pi(W) содержит идентичности.

LaTeX

$$$(\\pi W).ContainsIdentities$$$

Lean4

instance containsIdentities {J : Type w} {C : J → Type u} [∀ j, Category.{v} (C j)] (W : ∀ j, MorphismProperty (C j))
    [∀ j, (W j).ContainsIdentities] : (pi W).ContainsIdentities :=
  ⟨fun _ _ => MorphismProperty.id_mem _ _⟩

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