map_ofLE — Mathlib

English

If M is a matching and G ≤ G', then the image of M under the induced map is again a matching.

Русский

Если M — соответствие, и граф G вложим в G', то образ M под отображением маппинга сохраняет свойство соответствия.

LaTeX

$$$$ (M.map (Hom.ofLE hGG')).IsMatching $$$$

Lean4

theorem map_ofLE (h : M.IsMatching) (hGG' : G ≤ G') : (M.map (Hom.ofLE hGG')).IsMatching :=
  by
  intro _ hv
  obtain ⟨_, hv, hv'⟩ := Set.mem_image _ _ _ |>.mp hv
  obtain ⟨w, hw⟩ := h hv
  use w
  simpa using hv' ▸ hw

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