Theorem: SimpleGraph.subgraph_edge_subset (Turan4/Fedges.lean)

State before:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
G H : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableRel H.Adj
⊢ G ≤ H ↔ edgeFinset G ⊆ edgeFinset H
Tactic:
exact Iff.symm edgeFinset_subset_edgeFinset
State after:
no goals