mem_of_adj — Mathlib

English

There exists a pair (c, k) with c ∈ C, k ∈ K and G.Adj c k.

Русский

Существует пара (c, k) с c ∈ C, k ∈ K и G.Adj c k.

LaTeX

$$$$ \exists (ck: V \times V), ck.1 \in C \land ck.2 \in K \land G.Adj ck.1 ck.2 $$$$

Lean4

/-- Any vertex adjacent to a vertex of `C` and not lying in `K` must lie in `C`.
-/
theorem mem_of_adj : ∀ {C : G.ComponentCompl K} (c d : V), c ∈ C → d ∉ K → G.Adj c d → d ∈ C :=
  fun {C} c d ⟨cnK, h⟩ dnK cd =>
  ⟨dnK, by
    rw [← h, ConnectedComponent.eq]
    exact Adj.reachable cd.symm⟩

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