English
There is an order-preserving embedding from simple graphs on V into the power set of Sym2(V) given by mapping G to its edge set.
Русский
Существует монотонное вложение графов над V в множество подмножеств Sym^2(V), которое сопоставляет графу её множество ребер.
LaTeX
$$$$ \forall G,H:\ G \le H \iff E(G) \subseteq E(H). $$$$
Lean4
/-- The edges of G consist of the unordered pairs of vertices related by
`G.Adj`. This is the order embedding; for the edge set of a particular graph, see
`SimpleGraph.edgeSet`.
The way `edgeSet` is defined is such that `mem_edgeSet` is proved by `Iff.rfl`.
(That is, `s(v, w) ∈ G.edgeSet` is definitionally equal to `G.Adj v w`.)
-/
-- Porting note: We need a separate definition so that dot notation works.
def edgeSetEmbedding (V : Type*) : SimpleGraph V ↪o Set (Sym2 V) :=
OrderEmbedding.ofMapLEIff (fun G => Sym2.fromRel G.symm) fun _ _ =>
⟨fun h a b => @h s(a, b), fun h e => Sym2.ind (@h) e⟩
