internlm/Lean-Github huggingface dataset:
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
Tactic:
simp only [isOpen_compl_iff]
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₁ᶜ)ᶜ)
⊢ IsClosed (ρ '' G₂ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
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₁ᶜ)ᶜ)
⊢ IsClosed (ρ '' G₂ᶜ)
Tactic:
apply IsCompact.isClosed
Proof state after:
case open2.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₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsCompact (ρ '' G₂ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
case open2.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₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsCompact (ρ '' G₂ᶜ)
Tactic:
refine' IsCompact.image (IsClosed.isCompact _) ρ_cont
Proof state after:
case open2.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₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (G₂ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
case open2.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₂
open1 : IsOpen ((ρ '' G₁ᶜ)ᶜ)
⊢ IsClosed (G₂ᶜ)
Tactic:
simpa only [isClosed_compl_iff]
Proof state after:
no goals
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
Tactic:
rw [disjoint_compl_left_iff_subset]
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₂ᶜ)ᶜ)
⊢ (ρ '' G₂ᶜ)ᶜ ⊆ ρ '' G₁ᶜ
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
⊢ (ρ '' G₂ᶜ)ᶜ ⊆ ρ '' G₁ᶜ
Tactic:
refine' subset_trans (subset_image_compl ρ_surj) _
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₂ᶜ)ᶜ)
⊢ ρ '' G₂ᶜᶜ ⊆ ρ '' G₁ᶜ
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
⊢ ρ '' G₂ᶜᶜ ⊆ ρ '' G₁ᶜ
Tactic:
simp only [compl_compl, image_subset_iff]
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₂ᶜ)ᶜ)
⊢ G₂ ⊆ ρ ⁻¹' (ρ '' G₁ᶜ)
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
⊢ G₂ ⊆ ρ ⁻¹' (ρ '' G₁ᶜ)
Tactic:
refine' subset_trans _ (subset_preimage_image _ _)
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₂ᶜ)ᶜ)
⊢ G₂ ⊆ G₁ᶜ
Theorem: compact_to_T2_injective
Proof state before:
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₂ᶜ)ᶜ)
⊢ G₂ ⊆ G₁ᶜ
Tactic:
rw [← disjoint_compl_left_iff_subset]
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₂
Theorem: compact_to_T2_injective
Proof state before:
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₂
Tactic:
simpa only [compl_compl]
Proof state after:
no goals
Theorem: compact_to_T2_injective
Proof state before:
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₁
Tactic:
exact mem_image_of_mem _ hxG₁
Proof state after:
no goals
Theorem: compact_to_T2_injective
Proof state before:
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₂
Tactic:
rw [h_eq_im]
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₁
⊢ ρ y ∈ ρ '' G₂
Theorem: compact_to_T2_injective
Proof state before:
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₁
⊢ ρ y ∈ ρ '' G₂
Tactic:
exact mem_image_of_mem _ hyG₂
Proof state after:
no goals
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
⊢ ∃ E, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
haveI : CompactSpace <| D' φ f := isCompact_iff_compactSpace.mp (IsClosed.isCompact
  (isClosed_eq (Continuous.comp hφ continuous_fst) (Continuous.comp hf continuous_snd)))
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)
⊢ ∃ 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:
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)
⊢ ∃ E, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
let S := { E : Set (D' φ f) | CompactSpace E ∧ (π₁ φ f) '' E = univ}
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}
⊢ ∃ 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:
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, CompactSpace ↑E ∧ π₁ φ f '' E = univ ∧ ∀ (E₀ : Set ↑(D' φ f)), E₀ ⊂ E → CompactSpace ↑E₀ → π₁ φ f '' E₀ ≠ univ
Tactic:
have := zorn_superset S chain_cond
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}
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