containsIdentities — Mathlib

English

If W1 and W2 both contain identities, then their product property contains identities, with the identity mem given componentwise.

Русский

Если W1 и W2 оба содержат идентичности, то произведение W1×W2 тоже содержит идентичности, тождественные элементы задаются по компонентам.

LaTeX

$$$(W_1 \\mathrm{prod} W_2).ContainsIdentities$$

Lean4

instance containsIdentities {C₁ C₂ : Type*} [Category C₁] [Category C₂] (W₁ : MorphismProperty C₁)
    (W₂ : MorphismProperty C₂) [W₁.ContainsIdentities] [W₂.ContainsIdentities] : (prod W₁ W₂).ContainsIdentities :=
  ⟨fun _ => ⟨W₁.id_mem _, W₂.id_mem _⟩⟩

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