ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
⊢ v ∈ H.verts → SimpleGraph.singletonSubgraph G v ≤ H
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
⊢ SimpleGraph.singletonSubgraph G v ≤ H ↔ v ∈ H.verts
refine' ⟨fun h ↦ h.1 (Set.mem_singleton v), _⟩
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ SimpleGraph.singletonSubgraph G v ≤ H
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
⊢ v ∈ H.verts → SimpleGraph.singletonSubgraph G v ≤ H
intro h
case left
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ (SimpleGraph.singletonSubgraph G v).verts ⊆ H.verts

case right
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, Subgraph.Adj (SimpleGraph.singletonSubgraph G v) v_1 w → Subgraph.Adj H v_1 w
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ SimpleGraph.singletonSubgraph G v ≤ H
constructor
no goals
case left
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ (SimpleGraph.singletonSubgraph G v).verts ⊆ H.verts
rwa [singletonSubgraph_verts, Set.singleton_subset_iff]
no goals
case right
ι : Sort ?u.207802
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
v : V
H : Subgraph G
h : v ∈ H.verts
⊢ ∀ ⦃v_1 w : V⦄, Subgraph.Adj (SimpleGraph.singletonSubgraph G v) v_1 w → Subgraph.Adj H v_1 w
exact fun _ _ ↦ False.elim