internlm/Lean-Github huggingface dataset:
Theorem: image_subset_closure_compl_image_compl
Proof state before:
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
by_cases G_empty : G = ∅
Proof state after:
case pos
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)

case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case pos
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
simpa only [G_empty, image_empty] using empty_subset _
Proof state after:
no goals
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
⊢ ρ '' G ⊆ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
intro a ha
Proof state after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure ((ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ a ∈ closure ((ρ '' Gᶜ)ᶜ)
Tactic:
rw [mem_closure_iff]
Proof state after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → Set.Nonempty (o ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
⊢ ∀ (o : Set A), IsOpen o → a ∈ o → Set.Nonempty (o ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
intro N hN ha'
Proof state after:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
hN : IsOpen N
ha' : a ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
a : A
ha : a ∈ ρ '' G
N : Set A
hN : IsOpen N
ha' : a ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases (G.mem_image ρ a).mp ha with ⟨e, he, rfl⟩
Proof state after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have non_empty : (G ∩ ρ⁻¹' N).Nonempty := ⟨e, mem_inter he <| mem_preimage.mpr ha'⟩
Proof state after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have is_open : IsOpen <| G ∩ ρ⁻¹' N := hG.inter <| hN.preimage ρ_cont
Proof state after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have ne_top : ρ '' (G ∩ ρ⁻¹' N)ᶜ ≠ ⊤ := image_ne_top _ (compl_ne_univ.mpr non_empty)
                                          is_open.isClosed_compl
Proof state after:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases nonempty_compl.mpr ne_top with ⟨x, hx⟩
Proof state after:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have hx' : x ∈ (ρ '' Gᶜ)ᶜ := (compl_subset_compl.mpr <| image_subset ρ <|
                                compl_subset_compl.mpr <| G.inter_subset_left _) hx
Proof state after:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
x : A
hx : x ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : x ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
rcases ρ_surj x with ⟨y, rfl⟩
Proof state after:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
have hy : y ∈ G ∩ ρ⁻¹' N := not_mem_compl_iff.mp <| (not_imp_not.mpr <| mem_image_of_mem ρ) <|
                              (mem_compl_iff _ _).mp hx
Proof state after:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Theorem: image_subset_closure_compl_image_compl
Proof state before:
case neg.intro.intro.intro.intro
A : Type u_2
B : Type ?u.523
C : Type ?u.526
D : Type u_1
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₀ ≠ ⊤
G : Set ↑E
hG : IsOpen G
G_empty : ¬G = ∅
N : Set A
hN : IsOpen N
e : ↑E
he : e ∈ G
ha : ρ e ∈ ρ '' G
ha' : ρ e ∈ N
non_empty : Set.Nonempty (G ∩ ρ ⁻¹' N)
is_open : IsOpen (G ∩ ρ ⁻¹' N)
ne_top : ρ '' (G ∩ ρ ⁻¹' N)ᶜ ≠ ⊤
y : ↑E
hx : ρ y ∈ (ρ '' (G ∩ ρ ⁻¹' N)ᶜ)ᶜ
hx' : ρ y ∈ (ρ '' Gᶜ)ᶜ
hy : y ∈ G ∩ ρ ⁻¹' N
⊢ Set.Nonempty (N ∩ (ρ '' Gᶜ)ᶜ)
Tactic:
exact ⟨ρ y, mem_inter (mem_preimage.mp <| mem_of_mem_inter_right hy) hx'⟩
Proof state after:
no goals
Theorem: compact_to_T2_injective
Proof state before:
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
⊢ Function.Injective ρ
Tactic:
intro x y h_eq_im
Proof state after:
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
⊢ x = y
Theorem: compact_to_T2_injective
Proof state before:
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
⊢ x = y
Tactic:
by_contra h
Proof state after:
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
⊢ False
Theorem: compact_to_T2_injective
Proof state before:
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
⊢ False
Tactic:
rcases t2_separation h with ⟨G₁, G₂, hG₁, hG₂, hxG₁, hyG₂, 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₂
⊢ 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₂
⊢ False
Tactic:
have open1 : IsOpen ((ρ '' (G₁ᶜ))ᶜ)
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₂
⊢ 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₁ᶜ)ᶜ)
⊢ False