edgeSet_toSubgraph

Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.edgeSet_toSubgraph

English

The edge set of p.toSubgraph is exactly the set { e | e ∈ p.edges }.

Русский

Множество рёбер подграфа p.toSubgraph равно { e | e ∈ p.edges }.

LaTeX

$$$p.toSubgraph.edgeSet = \{ e \mid e \in p.edges \}$$$

Lean4

@[simp]
theorem edgeSet_toSubgraph (p : G.Walk u v) : p.toSubgraph.edgeSet = {e | e ∈ p.edges} :=
  Set.ext fun _ => p.mem_edges_toSubgraph

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru