internlm/Lean-Github huggingface dataset:
Theorem: exists_image_ne_top
Proof state before:
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
this : ∃ m, m ∈ S ∧ ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ m → a = m
⊢ ∃ E, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
rcases this with ⟨E, ⟨⟨hE₁,hE₂⟩, hE₃⟩⟩
Proof state after:
case intro.intro.intro
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ ∃ E, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
case intro.intro.intro
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ ∃ E, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
use E
Proof state after:
case intro.intro.intro
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
case intro.intro.intro
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
constructor
Proof state after:
case intro.intro.intro.left
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ CompactSpace ↑E

case intro.intro.intro.right
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
case intro.intro.intro.right
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
constructor
Proof state after:
case intro.intro.intro.right.left
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ π₁ φ f '' E = univ

case intro.intro.intro.right.right
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}
chain_cond :
  ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
E : Set ↑(D' φ f)
hE₃ : ∀ (a : Set ↑(D' φ f)), a ∈ S → a ⊆ E → a = E
hE₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
⊢ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
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}
⊢ ∀ (c : Set (Set ↑(D' φ f))),
    c ⊆ S → IsChain (fun x x_1 => x ⊆ x_1) c → ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ c → lb ⊆ s
Tactic:
intro Ch h hCh
Proof state after:
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
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → lb ⊆ s
Theorem: exists_image_ne_top
Proof state before:
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
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → lb ⊆ s
Tactic:
let M := sInter Ch
Proof state after:
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
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → lb ⊆ s
Theorem: exists_image_ne_top
Proof state before:
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
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → lb ⊆ s
Tactic:
use M
Proof state after:
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
⊢ M ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → M ⊆ s
Theorem: exists_image_ne_top
Proof state before:
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
⊢ M ∈ S ∧ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → M ⊆ s
Tactic:
constructor
Proof state after:
case left
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
⊢ M ∈ S

case right
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
⊢ ∀ (s : Set ↑(D' φ f)), s ∈ Ch → M ⊆ s
Theorem: exists_image_ne_top
Proof state before:
case left
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
⊢ M ∈ S
Tactic:
constructor
Proof state after:
case left.left
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
⊢ CompactSpace ↑M

case left.right
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
⊢ π₁ φ f '' M = univ
Theorem: exists_image_ne_top
Proof state before:
case left.left
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
⊢ CompactSpace ↑M
Tactic:
rw [←isCompact_iff_compactSpace]
Proof state after:
case left.left
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
⊢ IsCompact M
Theorem: exists_image_ne_top
Proof state before:
case left.left
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
⊢ IsCompact M
Tactic:
apply IsClosed.isCompact
Proof state after:
case left.left.h
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
⊢ IsClosed M