induce_eq_coe_induce_top — Mathlib

English

The induced subgraph on a set s is the same whether we view the ambient graph G or the top subgraph of G, via coercion.

Русский

Индуктивный подграф на множество s совпадает как внутри графа G, так и после переноса в верхний подграф через коэрцию.

LaTeX

$$$ G\\!\\text{.induce }s = ((\\top : G\\text{ Subgraph}).induce s)\\!\\text{.coe} $$$

Lean4

theorem _root_.SimpleGraph.induce_eq_coe_induce_top (s : Set V) : G.induce s = ((⊤ : G.Subgraph).induce s).coe :=
  by
  ext
  simp

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