V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ K ∩ ↑C ⊆ ∅
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ Disjoint K ↑C
rw [Set.disjoint_iff]
no goals
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ K ∩ ↑C ⊆ ∅
exact fun v ⟨vK, vC⟩ => vC.choose vK