internlm/Lean-Github huggingface dataset:
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ False
Tactic:
have open2 : IsOpen ((ρ '' (G₂ᶜ))ᶜ)
Proof state after:
case open2
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsOpen ((ρ '' G₂ᶜ)ᶜ)

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
have disj : Disjoint ((ρ '' (G₁ᶜ))ᶜ) ((ρ '' (G₂ᶜ))ᶜ)
Proof state after:
case disj
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
⊢ Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint ((ρ '' G₁ᶜ)ᶜ) ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
replace disj := disjoint_of_extremally_disconnected disj open1 open2
Proof state after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
⊢ False
Tactic:
have oups₁ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₁
Proof state after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
⊢ False
Tactic:
have oups₂ := image_subset_closure_compl_image_compl ρ_cont ρ_surj image_ne_top hG₂
Proof state after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
have mem₁ : ρ x ∈ ρ '' G₁
Proof state after:
case mem₁
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ ρ x ∈ ρ '' G₁

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ False
Tactic:
have mem₂ : ρ x ∈ ρ '' G₂
Proof state after:
case mem₂
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
⊢ ρ x ∈ ρ '' G₂

case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
⊢ False
Tactic:
have mem : ρ x ∈ (closure ((ρ '' G₁ᶜ)ᶜ)) ∩ (closure ((ρ '' G₂ᶜ)ᶜ)) := ⟨oups₁ mem₁, oups₂ mem₂⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
mem : ρ x ∈ closure ((ρ '' G₁ᶜ)ᶜ) ∩ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
open2 : IsOpen ((ρ '' G₂ᶜ)ᶜ)
disj : Disjoint (closure ((ρ '' G₁ᶜ)ᶜ)) (closure ((ρ '' G₂ᶜ)ᶜ))
oups₁ : ρ '' G₁ ⊆ closure ((ρ '' G₁ᶜ)ᶜ)
oups₂ : ρ '' G₂ ⊆ closure ((ρ '' G₂ᶜ)ᶜ)
mem₁ : ρ x ∈ ρ '' G₁
mem₂ : ρ x ∈ ρ '' G₂
mem : ρ x ∈ closure ((ρ '' G₁ᶜ)ᶜ) ∩ closure ((ρ '' G₂ᶜ)ᶜ)
⊢ False
Tactic:
exact (disj.ne_of_mem mem.1 mem.2) rfl
Proof state after:
no goals
Theorem: compact_to_T2_injective
Proof state before:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsOpen ((ρ '' G₁ᶜ)ᶜ)
Tactic:
simp only [isOpen_compl_iff]
Proof state after:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (ρ '' G₁ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
case open1
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (ρ '' G₁ᶜ)
Tactic:
apply IsCompact.isClosed
Proof state after:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsCompact (ρ '' G₁ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsCompact (ρ '' G₁ᶜ)
Tactic:
refine' IsCompact.image (IsClosed.isCompact _) ρ_cont
Proof state after:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (G₁ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
case open1.hs
A : Type u_1
B : Type ?u.3855
C : Type ?u.3858
D : Type u_2
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✝² : ExtremallyDisconnected A
inst✝¹ : T2Space ↑E
inst✝ : CompactSpace ↑E
x y : ↑E
h_eq_im : ρ x = ρ y
h : ¬x = y
G₁ G₂ : Set ↑E
hG₁ : IsOpen G₁
hG₂ : IsOpen G₂
hxG₁ : x ∈ G₁
hyG₂ : y ∈ G₂
hG : Disjoint G₁ G₂
⊢ IsClosed (G₁ᶜ)
Tactic:
simpa only [isClosed_compl_iff]
Proof state after:
no goals