V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ∃ x, x ∈ ↑C ∧ x ∈ ↑D
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D
rw [Set.not_disjoint_iff]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D → ∃ x, x ∈ ↑C ∧ x ∈ ↑D

case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ (∃ x, x ∈ ↑C ∧ x ∈ ↑D) → hom h C = D
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ∃ x, x ∈ ↑C ∧ x ∈ ↑D
constructor
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ∃ x, x ∈ ↑C ∧ x ∈ ↑(hom h C)
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D → ∃ x, x ∈ ↑C ∧ x ∈ ↑D
rintro rfl
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x : V
xnL : ¬x ∈ L
⊢ ∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑(hom h (componentComplMk G xnL))
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ∃ x, x ∈ ↑C ∧ x ∈ ↑(hom h C)
refine C.ind fun x xnL => ?_
no goals
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x : V
xnL : ¬x ∈ L
⊢ ∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑(hom h (componentComplMk G xnL))
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
x : V
xnL : ¬x ∈ L
⊢ (∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑D) → hom h (componentComplMk G xnL) = D
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ (∃ x, x ∈ ↑C ∧ x ∈ ↑D) → hom h C = D
refine C.ind fun x xnL => ?_
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G xnL) = componentComplMk G w✝
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
x : V
xnL : ¬x ∈ L
⊢ (∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑D) → hom h (componentComplMk G xnL) = D
rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G w✝¹) = componentComplMk G w✝
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G xnL) = componentComplMk G w✝
rw [← e₁]
no goals
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G w✝¹) = componentComplMk G w✝
rfl