subgraphOfAdj_eq_induce — Mathlib

English

If two vertices v and w are adjacent in G, then the subgraph of G obtained from that edge, G.subgraphOfAdj hvw, is the same as the induced subgraph of G on {v,w}.

Русский

Пусть вершины v и w смежны в G. Подграф G, образованный по ребру hvw, равен индуцированному подграфу G на множестве {v, w}.

LaTeX

$$$ G.subgraphOfAdj hvw = (\top : G.Subgraph).induce \{ v, w \}$$$

Lean4

theorem subgraphOfAdj_eq_induce {v w : V} (hvw : G.Adj v w) : G.subgraphOfAdj hvw = (⊤ : G.Subgraph).induce { v, w } :=
  by
  ext
  · simp
  · constructor
    · intro h
      simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h
      obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h <;> simp [hvw, hvw.symm]
    · intro h
      simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h
      obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h <;>
        first
        | exact (ha.ne rfl).elim
        | simp

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