spanningCoe_sup_edge_le — Mathlib

English

Let H be a subgraph of G ⊔ edge s t. If H does not contain the edge s t (i.e., ¬H.Adj s t), then H.spanningCoe ≤ G.

Русский

Пусть H — подграф графа G ⊔ edge s t. Если H не содержит ребра s t (¬H.Adj s t), то H.spanningCoe ≤ G.

LaTeX

$$$\\forall H : Subgraph (G \\sqcup edge\\ s\\ t), \\neg H.Adj\\ s\\ t \\Rightarrow H.spanningCoe \\le G$$$

Lean4

theorem spanningCoe_sup_edge_le {H : Subgraph (G ⊔ edge s t)} (h : ¬H.Adj s t) : H.spanningCoe ≤ G :=
  by
  intro v w hvw
  have := hvw.adj_sub
  simp only [Subgraph.spanningCoe_adj, SimpleGraph.sup_adj, SimpleGraph.edge_adj] at *
  by_cases hs : s(v, w) = s(s, t)
  · exact (h ((Subgraph.adj_congr_of_sym2 hs).mp hvw)).elim
  · aesop

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