coeSubgraph_restrict_eq — Mathlib

English

Let H and H' be subgraphs of G. Then the restriction of H to H' equals the intersection H ∩ H' (i.e., the greatest subgraph contained in both).

Русский

Пусть H и H' — подграфы графа G. Тогда ограничение H до H' равно пересечению H и H' (наибольший подграф, входящий в оба).

LaTeX

$$$ \\operatorname{Subgraph.coeSubgraph}(H\\restriction H') = H \\sqcap H' $$$

Lean4

theorem coeSubgraph_restrict_eq {H : G.Subgraph} (H' : G.Subgraph) : Subgraph.coeSubgraph (H.restrict H') = H ⊓ H' :=
  by
  ext
  · simp
  · simp_rw [coeSubgraph_adj, restrict_adj]
    simp only [exists_and_left, exists_prop, inf_adj, and_congr_right_iff]
    intro h
    simp [H.edge_vert h, H.edge_vert h.symm]

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