case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
⊢ ∃ i, V i ⊆ U
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
⊢ ∃ i, V i ⊆ U
obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
this : ∃ i, V i ⊆ W
⊢ ∃ i, V i ⊆ U

case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
⊢ ∃ i, V i ⊆ W
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
⊢ ∃ i, V i ⊆ U
suffices : ∃ i, V i ⊆ W
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), ¬V i ⊆ W
⊢ False
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
⊢ ∃ i, V i ⊆ W
by_contra' H
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
⊢ False
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), ¬V i ⊆ W
⊢ False
replace H : ∀ i, (V i ∩ Wᶜ).Nonempty := fun i => Set.inter_compl_nonempty_iff.mpr (H i)
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
this : Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
⊢ False
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
⊢ False
have : (⋂ i, V i ∩ Wᶜ).Nonempty := by
  refine'
    IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ (fun i j => _) H
      (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
      (hV_closed i).inter W_op.isClosed_compl
  rcases hV i j with ⟨k, hki, hkj⟩
  refine' ⟨k, ⟨fun x => _, fun x => _⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
    tauto
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
this✝ : Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
this : ¬(⋂ (i : ι), V i) ⊆ W
⊢ False
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
this : Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
⊢ False
have : ¬(⋂ i : ι, V i) ⊆ W := by simpa [← iInter_inter, inter_compl_nonempty_iff]
no goals
case this
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
this✝ : Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
this : ¬(⋂ (i : ι), V i) ⊆ W
⊢ False
contradiction
no goals
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
this : ∃ i, V i ⊆ W
⊢ ∃ i, V i ⊆ U
exact this.imp fun i hi => hi.trans hWU
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
i j : ι
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x x_1 => x ⊇ x_1) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
⊢ Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
refine'
  IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ (fun i j => _) H
    (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
    (hV_closed i).inter W_op.isClosed_compl
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x x_1 => x ⊇ x_1) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
i j : ι
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x x_1 => x ⊇ x_1) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
rcases hV i j with ⟨k, hki, hkj⟩
no goals
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
i j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
⊢ ∃ z, (fun x x_1 => x ⊇ x_1) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x x_1 => x ⊇ x_1) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
refine' ⟨k, ⟨fun x => _, fun x => _⟩⟩ <;> simp only [and_imp, mem_inter_iff, mem_compl_iff] <;>
  tauto
no goals
α : Type u
β : Type v
ι✝ : Type ?u.36248
π : ι✝ → Type ?u.36253
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
ι : Type u_1
inst✝ : Nonempty ι
V : ι → Set α
hV : Directed (fun x x_1 => x ⊇ x_1) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed (V i)
U : Set α
hU : ∀ (x : α), (x ∈ ⋂ (i : ι), V i) → U ∈ 𝓝 x
W : Set α
hsubW : (⋂ (i : ι), V i) ⊆ W
W_op : IsOpen W
hWU : W ⊆ U
H : ∀ (i : ι), Set.Nonempty (V i ∩ Wᶜ)
this : Set.Nonempty (⋂ (i : ι), V i ∩ Wᶜ)
⊢ ¬(⋂ (i : ι), V i) ⊆ W
simpa [← iInter_inter, inter_compl_nonempty_iff]