V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ Disjoint ↑C ↑D
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Pairwise fun C D => Disjoint ↑C ↑D
rintro C D ne
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ Disjoint ↑C ↑D
rw [Set.disjoint_iff]
no goals
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅
exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)