Theorem: exists_image_ne_top
Proof state before:
case pos
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
E : Set D
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
inst✝⁵ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁴ : T2Space A
inst✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
⊢ π₁ φ f '' M = univ

case neg
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
E : Set D
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
inst✝⁵ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁴ : T2Space A
inst✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : ¬Nonempty ↑Ch
⊢ π₁ φ f '' M = univ
Tactic:
rotate_left 1
Proof state after:
case neg
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
E : Set D
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
inst✝⁵ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁴ : T2Space A
inst✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : ¬Nonempty ↑Ch
⊢ π₁ φ f '' M = univ

case pos
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.12569
E : Set D
inst✝⁸ : TopologicalSpace A
inst✝⁷ : TopologicalSpace B
inst✝⁶ : TopologicalSpace C
inst✝⁵ : TopologicalSpace D
ρ : ↑E → A
ρ_cont : Continuous ρ
ρ_surj : Function.Surjective ρ
π : D → A
π_cont : Continuous π
π_surj : Function.Surjective π
image_ne_top : ∀ (E₀ : Set ↑E), E₀ ≠ ⊤ → IsClosed E₀ → ρ '' E₀ ≠ ⊤
inst✝⁴ : T2Space A
inst✝³ : CompactSpace A
inst✝² : T2Space B
inst✝¹ : CompactSpace B
inst✝ : T2Space C
φ : A → C
f : B → C
hφ : Continuous φ
hf : Continuous f
hf' : Function.Surjective f
this : CompactSpace ↑(D' φ f)
S : Set (Set ↑(D' φ f)) := {E | CompactSpace ↑E ∧ π₁ φ f '' E = univ}
Ch : Set (Set ↑(D' φ f))
h : Ch ⊆ S
hCh : IsChain (fun x x_1 => x ⊆ x_1) Ch
M : Set ↑(D' φ f) := ⋂₀ Ch
h₂ : Nonempty ↑Ch
⊢ π₁ φ f '' M = univ