English
If G is alternating with respect to G' and certain adjacency transfer conditions hold (no adjacency between u and x in G'), then adding the edge (u, x) to G preserves the alternating property with respect to G'.
Русский
Если G чередуется относительно G' и выполняются условия переноса смежности (нет смежности между u и x в G'), то добавление ребра (u, x) к G сохраняет чередование относительно G'.
LaTeX
$$$ G.IsAlternating G' \land \neg G'.Adj u x \land (\forall u', u' \neq u \to G.Adj x u' \to G'.Adj x u') \land (\forall x', x' \neq x \to G.Adj x' u \to G'.Adj x' u) \Rightarrow (G \uplus edge\ u x).IsAlternating G' $$$
Lean4
theorem sup_edge {u x : V} (halt : G.IsAlternating G') (hnadj : ¬G'.Adj u x)
(hu' : ∀ u', u' ≠ u → G.Adj x u' → G'.Adj x u') (hx' : ∀ x', x' ≠ x → G.Adj x' u → G'.Adj x' u) :
(G ⊔ edge u x).IsAlternating G' := by
by_cases hadj : G.Adj u x
· rwa [sup_edge_of_adj G hadj]
intro v w w' hww' hvw hvv'
simp only [sup_adj, edge_adj] at hvw hvv'
obtain hl | hr := hvw <;> obtain h1 | h2 := hvv'
· exact halt hww' hl h1
· rw [G'.adj_congr_of_sym2 (by aesop : s(v, w') = s(u, x))]
simp only [hnadj, not_false_eq_true, iff_true]
rcases h2.1 with ⟨h2l1, h2l2⟩ | ⟨h2r1, h2r2⟩
· subst h2l1 h2l2
exact (hx' _ hww' hl.symm).symm
· simp_all
· rw [G'.adj_congr_of_sym2 (by aesop : s(v, w) = s(u, x))]
simp only [hnadj, false_iff, not_not]
rcases hr.1 with ⟨hrl1, hrl2⟩ | ⟨hrr1, hrr2⟩
· subst hrl1 hrl2
exact (hx' _ hww'.symm h1.symm).symm
· aesop
· aesop
