English
Given two disjoint sets and an equivalence between them, there exists a subgraph on their union that is a matching.
Русский
Пусть даны два непересекающихся множества и эквивалентность между ними; существует подграф их объединения, являющийся соответствием.
LaTeX
$$$$\\exists M : Subgraph G, M.verts = s \\cup t \\land M.IsMatching$$$$
Lean4
theorem exists_of_disjoint_sets_of_equiv {s t : Set V} (h : Disjoint s t) (f : s ≃ t) (hadj : ∀ v : s, G.Adj v (f v)) :
∃ M : Subgraph G, M.verts = s ∪ t ∧ M.IsMatching :=
by
use {
verts := s ∪ t
Adj := fun v w ↦ (∃ h : v ∈ s, f ⟨v, h⟩ = w) ∨ (∃ h : w ∈ s, f ⟨w, h⟩ = v)
adj_sub := by
intro v w h
obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
· exact hadj ⟨v, _⟩
· exact (hadj ⟨w, _⟩).symm
edge_vert := by aesop }
simp only [Subgraph.IsMatching, Set.mem_union, true_and]
intro v hv
rcases hv with hl | hr
· use f ⟨v, hl⟩
simp only [hl, exists_const, true_or, exists_true_left, true_and]
rintro y (rfl | ⟨hys, rfl⟩)
· rfl
· exact (h.ne_of_mem hl (f ⟨y, hys⟩).coe_prop rfl).elim
· use f.symm ⟨v, hr⟩
simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_prop, exists_const, or_true, true_and]
rintro y (⟨hy, rfl⟩ | ⟨hy, rfl⟩)
· exact (h.ne_of_mem hy hr rfl).elim
· simp
