singletonSubgraph_le_iff — Mathlib

English

The inclusion of a singleton subgraph is characterized by membership of the vertex in the target's vertex set.

Русский

Включение одиночного подграфа характеризуется принадлежностью вершины целевому множеству вершин.

LaTeX

$$$(G.singletonSubgraph v) \le H \iff v \in H.verts$$$

Lean4

@[simp]
theorem singletonSubgraph_le_iff (v : V) (H : G.Subgraph) : G.singletonSubgraph v ≤ H ↔ v ∈ H.verts :=
  by
  refine ⟨fun h ↦ h.1 (Set.mem_singleton v), ?_⟩
  intro h
  constructor
  · rwa [singletonSubgraph_verts, Set.singleton_subset_iff]
  · exact fun _ _ ↦ False.elim

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