w_prod_snd — Mathlib

English

The costructured arrows' preimage under the projection is small when restricted to a locally small family.

Русский

Предобраз проекции коструктурированных стрелок мал по отношению к локально малой семье.

LaTeX

$$Small (Set.preimage (StructuredArrow.proj S T).obj 𝒢).Elem$$

Lean4

@[reassoc (attr := simp)]
theorem w_prod_snd {A B : CostructuredArrow (S.prod S') (T, T')} (f : A ⟶ B) : S'.map f.left.2 ≫ B.hom.2 = A.hom.2 :=
  congr_arg _root_.Prod.snd (CostructuredArrow.w f)

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