image_coe_edgeSet_coe — Mathlib

English

The image of the coe-edgeSet under the map Sym2.map Subtype.val equals the underlying edge set of the subgraph.

Русский

Образ множества ребер подграфа через отображение Sym2.map равен исходному множеству ребер подграфа.

LaTeX

$$$\\mathrm{Sym2.map}(\\mathrm{Subtype.val})[G'.\\mathrm{coe}.\\mathrm{edgeSet}] = G'.\\mathrm{edgeSet}$$$

Lean4

theorem image_coe_edgeSet_coe (G' : G.Subgraph) : Sym2.map (↑) '' G'.coe.edgeSet = G'.edgeSet :=
  by
  rw [edgeSet_coe, Set.image_preimage_eq_iff]
  rintro e he
  induction e using Sym2.ind with
  | h a b =>
    rw [Subgraph.mem_edgeSet] at he
    exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq ..⟩

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