isCycles_spanningCoe_toSubgraph_sup_edge

English

See previous; the construction yields a cycle after adding the extra edge to spanningCoe.

Русский

См. предыдущее: конструирование даёт цикл после добавления дополнительного ребра к spanningCoe.

LaTeX

$$(p.toSubgraph.spanningCoe \cup edge(v,u)).IsCycles$$

Lean4

theorem isCycles_spanningCoe_toSubgraph_sup_edge {u v} {p : G.Walk u v} (hp : p.IsPath) (h : u ≠ v)
    (hs : s(v, u) ∉ p.edges) : (p.toSubgraph.spanningCoe ⊔ edge v u).IsCycles :=
  by
  let c := (p.mapLe (OrderTop.le_top G)).cons (by simp [h.symm] : (completeGraph V).Adj v u)
  have : p.toSubgraph.spanningCoe ⊔ edge v u = c.toSubgraph.spanningCoe :=
    by
    ext w x
    simp only [sup_adj, Subgraph.spanningCoe_adj, completeGraph_eq_top, edge_adj, c, Walk.toSubgraph, Subgraph.sup_adj,
      subgraphOfAdj_adj, adj_toSubgraph_mapLe]
    aesop
  exact this ▸ IsCycle.isCycles_spanningCoe_toSubgraph (by simp [Walk.cons_isCycle_iff, c, hp, hs])

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