induce_self_verts

Mathlib.Combinatorics.SimpleGraph.Subgraph

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Subgraph.induce_self_verts

← MathLib Explorer

English

Inducing on the vertex set of G' returns G' itself.

Русский

Индукция по множеству вершин G' возвращает сам G'.

LaTeX

$$$ G'.induce G'.verts = G' $$$

Lean4

@[simp]
theorem induce_self_verts : G'.induce G'.verts = G' := by
  ext
  · simp
  · constructor <;> simp +contextual only [induce_adj, imp_true_iff, and_true]
    exact fun ha ↦ ⟨G'.edge_vert ha, G'.edge_vert ha.symm⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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