internlm/Lean-Github huggingface dataset:
Theorem: exists_image_ne_top
Proof state before:
case refine'_2
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
x : A
x✝ : x ∈ univ
Z : ↑Ch → Set ↑(D' φ f) := fun X => ↑X ∩ π₁ φ f ⁻¹' {x}
assumps : ∀ (i : ↑Ch), Set.Nonempty (Z i) ∧ IsCompact (Z i) ∧ IsClosed (Z i)
⊢ ∀ ⦃x_1 y : Set ↑(D' φ f)⦄, x_1 ⊇ y → x_1 ∩ π₁ φ f ⁻¹' {x} ⊇ y ∩ π₁ φ f ⁻¹' {x}
Tactic:
exact fun ⦃x y⦄ a => inter_subset_inter_left _ a
Proof state after:
no goals
Theorem: exists_image_ne_top
Proof state before:
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
Tactic:
intro X hX
Proof state after:
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
X : Set ↑(D' φ f)
hX : X ∈ Ch
⊢ M ⊆ X
Theorem: exists_image_ne_top
Proof state before:
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
X : Set ↑(D' φ f)
hX : X ∈ Ch
⊢ M ⊆ X
Tactic:
exact sInter_subset_of_mem hX
Proof state after:
no goals
Theorem: exists_image_ne_top
Proof state before:
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
Tactic:
exact hE₁
Proof state after:
no goals
Theorem: exists_image_ne_top
Proof state before:
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
Tactic:
exact hE₂
Proof state after:
no goals
Theorem: exists_image_ne_top
Proof state before:
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
Tactic:
intro E₀ h₁ h₂
Proof state after:
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)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
⊢ π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
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)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
⊢ π₁ φ f '' E₀ ≠ univ
Tactic:
replace hE₃ := hE₃ E₀
Proof state after:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
hE₃ : E₀ ∈ S → E₀ ⊆ E → E₀ = E
⊢ π₁ φ f '' E₀ ≠ univ
Theorem: exists_image_ne_top
Proof state before:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
hE₃ : E₀ ∈ S → E₀ ⊆ E → E₀ = E
⊢ π₁ φ f '' E₀ ≠ univ
Tactic:
by_contra h₃
Proof state after:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
hE₃ : E₀ ∈ S → E₀ ⊆ E → E₀ = E
h₃ : π₁ φ f '' E₀ = univ
⊢ False
Theorem: exists_image_ne_top
Proof state before:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
hE₃ : E₀ ∈ S → E₀ ⊆ E → E₀ = E
h₃ : π₁ φ f '' E₀ = univ
⊢ False
Tactic:
replace hE₃ := hE₃ (And.intro h₂ h₃) (subset_of_ssubset h₁)
Proof state after:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
h₃ : π₁ φ f '' E₀ = univ
hE₃ : E₀ = E
⊢ False
Theorem: exists_image_ne_top
Proof state before:
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₁ : CompactSpace ↑E
hE₂ : π₁ φ f '' E = univ
E₀ : Set ↑(D' φ f)
h₁ : E₀ ⊂ E
h₂ : CompactSpace ↑E₀
h₃ : π₁ φ f '' E₀ = univ
hE₃ : E₀ = E
⊢ False
Tactic:
exact (ne_of_ssubset h₁) hE₃
Proof state after:
no goals
Theorem: gleason_diagram_commutes
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun) ∧
    f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Tactic:
constructor
Proof state after:
case left
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun)

case right
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ f ∘ restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun = φ
Theorem: gleason_diagram_commutes
Proof state before:
case left
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f) ∘ (ρ' hφ hf hf').toEquiv.invFun)
Tactic:
refine' Continuous.comp _ _
Proof state after:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f))

case left.refine'_2
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (ρ' hφ hf hf').toEquiv.invFun
Theorem: gleason_diagram_commutes
Proof state before:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (restrict (E' hφ hf hf') (π₂ φ f))
Tactic:
refine' ContinuousOn.restrict _
Proof state after:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ ContinuousOn (π₂ φ f) (E' hφ hf hf')
Theorem: gleason_diagram_commutes
Proof state before:
case left.refine'_1
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ ContinuousOn (π₂ φ f) (E' hφ hf hf')
Tactic:
apply Continuous.continuousOn
Proof state after:
case left.refine'_1.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (π₂ φ f)
Theorem: gleason_diagram_commutes
Proof state before:
case left.refine'_1.h
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (π₂ φ f)
Tactic:
exact Continuous.comp continuous_snd continuous_subtype_val
Proof state after:
no goals
Theorem: gleason_diagram_commutes
Proof state before:
case left.refine'_2
A : Type u_1
B : Type u_2
C : Type u_3
D : Type ?u.44712
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
inst✝ : ExtremallyDisconnected A
⊢ Continuous (ρ' hφ hf hf').toEquiv.invFun
Tactic:
exact (Homeomorph.continuous (Homeomorph.symm (ρ' hφ hf hf')))
Proof state after:
no goals