English
Restriction of a homomorphism: given a subgraph G' ≤ G and a homomorphism f from G' to F, one can restrict f to any sub-subgraph G'' ≤ G' to obtain a homomorphism G'' → F.
Русский
Ограничение гомоморфизма: дано подграф G' ≤ G и гомоморфизм f: G' → F, можно ограничить f до подграфа G'' ≤ G', чтобы получить гомоморфизм G'' → F.
LaTeX
$$$$ \\forall G',G'' : G.Finsubgraph\\; (h: G'' \\le G')\\; (f: G' \\tofg F),\\; G'' \\tofg F. $$$$
Lean4
/-- Given a homomorphism from a subgraph to `F`, construct its restriction to a sub-subgraph. -/
def restrict {G' G'' : G.Finsubgraph} (h : G'' ≤ G') (f : G' →fg F) : G'' →fg F :=
by
refine ⟨fun ⟨v, hv⟩ => f.toFun ⟨v, h.1 hv⟩, ?_⟩
rintro ⟨u, hu⟩ ⟨v, hv⟩ huv
exact f.map_rel' (h.2 huv)