map_snd — Mathlib

English

For p ≃ F.Elements and any morphism f: p ⟶ q, the second component is preserved by F.map on the morphism: (F.map f.val) p.2 = q.2.

Русский

Для p, q ∈ F.Elements и любой морфизм p ⟶ q выполняется: (F.map f.val) p.2 = q.2.

LaTeX

$$$\\forall {F : C \\to Type_w} {p q : F.Elements} (f : p \\to q), (F.map f.val) p.2 = q.2$$

Lean4

@[simp]
theorem map_snd {F : C ⥤ Type w} {p q : F.Elements} (f : p ⟶ q) : (F.map f.val) p.2 = q.2 :=
  f.property

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