coeSubgraph_le — Mathlib

English

For H : G.Subgraph and H' : H.coe.Subgraph, Subgraph.coeSubgraph H' ≤ H; i.e., taking a co-subgraph and mapping back is contained in the original subgraph.

Русский

Для H : G.Subgraph и H' : H.coe.Subgraph, Subgraph.coeSubgraph H' ≤ H; т.е. отображение обратно в оригинальный подграф остаётся внутри него.

LaTeX

$$$\\forall H : G.Subgraph, \\forall H' : H.\\mathrm{coe.Subgraph}, \\mathrm{Subgraph.coeSubgraph} H' \\le H$$$

Lean4

theorem coeSubgraph_le {H : G.Subgraph} (H' : H.coe.Subgraph) : Subgraph.coeSubgraph H' ≤ H :=
  by
  constructor
  · simp
  · rintro v w ⟨_, _, h, rfl, rfl⟩
    exact H'.adj_sub h

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