map — Mathlib

English

If f is an injective homomorphism between graphs and M is a matching in G, then the image M.map f is a matching in G'.

Русский

Если f — внедренное отображение между графами и M — соответствие в G, то образ M.map f — соответствие в G'.

LaTeX

$$$$ (M.map f).IsMatching $$$$

Lean4

protected theorem map {G' : SimpleGraph W} {M : Subgraph G} (f : G →g G') (hf : Injective f) (hM : M.IsMatching) :
    (M.map f).IsMatching := by
  rintro _ ⟨v, hv, rfl⟩
  obtain ⟨v', hv'⟩ := hM hv
  use f v'
  refine ⟨⟨v, v', hv'.1, rfl, rfl⟩, ?_⟩
  rintro _ ⟨w, w', hw, hw', rfl⟩
  cases hf hw'.symm
  rw [hv'.2 w' hw]

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