ofHom — Mathlib

English

Typecheck a FrameHom as a morphism in Frm; given frames X and Y, FrameHom X Y yields Frm.of X ⟶ Frm.of Y.

Русский

Типизация FrameHom как морфизма в Frm; для рам X и Y, FrameHom X Y дает Frm.of X ⟶ Frm.of Y.

LaTeX

$$ofHom : {X Y : Type u} → FrameHom X Y → Frm.of X ⟶ Frm.of Y$$

Lean4

/-- Typecheck a `FrameHom` as a morphism in `Frm`. -/
abbrev ofHom {X Y : Type u} [Frame X] [Frame Y] (f : FrameHom X Y) : of X ⟶ of Y :=
  ConcreteCategory.ofHom (C := Frm) f

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