restrict — Mathlib

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)

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