coeSubgraph — Mathlib

English

If M is a matching on a subgraph of G, then the subgraph induced by M via the coe map is also a matching.

Русский

Если M — соответствие подграфа G.coe, то сопутствующий подграф сохраняет свойство соответствия.

LaTeX

$$$$(Subgraph.coeSubgraph M).IsMatching$$$$

Lean4

theorem coeSubgraph {G' : Subgraph G} {M : Subgraph G'.coe} (hM : M.IsMatching) : (Subgraph.coeSubgraph M).IsMatching :=
  by
  intro _ hv
  obtain ⟨w, hw⟩ := hM <| Set.mem_of_mem_image_val <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
  use w
  refine ⟨?_, fun y hy => ?_⟩
  · obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
    simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]
    exact ⟨hv.2 ▸ v.2, hw.1⟩
  · obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy
    rw [← hw.2 ⟨y, hw'⟩ hvw]

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