α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClosed (Z ∩ a)
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClopen (Z ∩ a)
refine' ⟨IsOpen.inter h.1 ha, _⟩
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ IsClosed (Z ∩ a)
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
⊢ IsClosed (Z ∩ a)
have : IsClosed (Z ∩ bᶜ) := IsClosed.inter h.2 (isClosed_compl_iff.2 hb)
case h.e'_3
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ Z ∩ a = Z ∩ bᶜ
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ IsClosed (Z ∩ a)
convert this using 1
case h.e'_3
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ Z ∩ bᶜ ⊆ Z ∩ a
case h.e'_3
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ Z ∩ a = Z ∩ bᶜ
refine' (inter_subset_inter_right Z hab.subset_compl_right).antisymm _
case h.e'_3.intro
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
x : α
hx₁ : x ∈ Z
hx₂ : x ∈ bᶜ
⊢ x ∈ Z ∩ a
case h.e'_3
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
⊢ Z ∩ bᶜ ⊆ Z ∩ a
rintro x ⟨hx₁, hx₂⟩
no goals
case h.e'_3.intro
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
x : α
hx₁ : x ∈ Z
hx₂ : x ∈ bᶜ
⊢ x ∈ Z ∩ a
exact ⟨hx₁, by simpa [not_mem_of_mem_compl hx₂] using cover hx₁⟩
no goals
α : Type u
β : Type v
ι : Type ?u.176436
π : ι → Type ?u.176441
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t Z a b : Set α
h : IsClopen Z
cover : Z ⊆ a ∪ b
ha : IsOpen a
hb : IsOpen b
hab : Disjoint a b
this : IsClosed (Z ∩ bᶜ)
x : α
hx₁ : x ∈ Z
hx₂ : x ∈ bᶜ
⊢ x ∈ a
simpa [not_mem_of_mem_compl hx₂] using cover hx₁