α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
⊢ ι → Set.Nonempty (⋂ (i : ι), Z i)
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
⊢ Set.Nonempty (⋂ (i : ι), Z i)
apply hι.elim
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
⊢ Set.Nonempty (⋂ (i : ι), Z i)
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
⊢ ι → Set.Nonempty (⋂ (i : ι), Z i)
intro i₀
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ Set.Nonempty (⋂ (i : ι), Z i)
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
⊢ Set.Nonempty (⋂ (i : ι), Z i)
let Z' i := Z i ∩ Z i₀
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ Set.Nonempty (⋂ (i : ι), Z' i)
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ Set.Nonempty (⋂ (i : ι), Z i)
suffices (⋂ i, Z' i).Nonempty by
  exact this.mono (iInter_mono fun i => inter_subset_left (Z i) (Z i₀))
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ (⋂ (i : ι), Z' i) ≠ ∅
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ Set.Nonempty (⋂ (i : ι), Z' i)
rw [nonempty_iff_ne_empty]
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
⊢ (⋂ (i : ι), Z' i) ≠ ∅
intro H
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
⊢ ∃ t, (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅

case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
⊢ False
obtain ⟨t, ht⟩ : ∃ t : Finset ι, (Z i₀ ∩ ⋂ i ∈ t, Z' i) = ∅
case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
⊢ ∃ t, (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅

case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
⊢ False
exact (hZc i₀).elim_finite_subfamily_closed Z' (fun i => IsClosed.inter (hZcl i) (hZcl i₀))
  (by rw [H, inter_empty])
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
⊢ False
case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
⊢ False
obtain ⟨i₁, hi₁⟩ : ∃ i₁ : ι, Z i₁ ⊆ Z i₀ ∧ ∀ i ∈ t, Z i₁ ⊆ Z' i := by
  rcases Directed.finset_le hZd t with ⟨i, hi⟩
  rcases hZd i i₀ with ⟨i₁, hi₁, hi₁₀⟩
  refine ⟨i₁, hi₁₀, fun j hj => ?_⟩
  exact subset_inter (hi₁.trans (hi j hj)) hi₁₀
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
⊢ Set.Nonempty (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i)
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
⊢ False
suffices (Z i₀ ∩ ⋂ i ∈ t, Z' i).Nonempty by
  rw [nonempty_iff_ne_empty] at this
  contradiction
no goals
case intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
⊢ Set.Nonempty (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i)
exact (hZn i₁).mono (subset_inter hi₁.left <| subset_iInter₂ hi₁.right)
no goals
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
this : Set.Nonempty (⋂ (i : ι), Z' i)
⊢ Set.Nonempty (⋂ (i : ι), Z i)
exact this.mono (iInter_mono fun i => inter_subset_left (Z i) (Z i₀))
no goals
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
⊢ (Z i₀ ∩ ⋂ (i : ι), Z' i) = ∅
rw [H, inter_empty]
case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
⊢ ∃ i₁, Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
⊢ ∃ i₁, Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
rcases Directed.finset_le hZd t with ⟨i, hi⟩
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
i₁ : ι
hi₁ : Z i ⊇ Z i₁
hi₁₀ : Z i₀ ⊇ Z i₁
⊢ ∃ i₁, Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
case intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
⊢ ∃ i₁, Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
rcases hZd i i₀ with ⟨i₁, hi₁, hi₁₀⟩
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
i₁ : ι
hi₁ : Z i ⊇ Z i₁
hi₁₀ : Z i₀ ⊇ Z i₁
j : ι
hj : j ∈ t
⊢ Z i₁ ⊆ Z' j
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
i₁ : ι
hi₁ : Z i ⊇ Z i₁
hi₁₀ : Z i₀ ⊇ Z i₁
⊢ ∃ i₁, Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
refine ⟨i₁, hi₁₀, fun j hj => ?_⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i : ι
hi : ∀ (i_1 : ι), i_1 ∈ t → Z i_1 ⊇ Z i
i₁ : ι
hi₁ : Z i ⊇ Z i₁
hi₁₀ : Z i₀ ⊇ Z i₁
j : ι
hj : j ∈ t
⊢ Z i₁ ⊆ Z' j
exact subset_inter (hi₁.trans (hi j hj)) hi₁₀
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
this : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) ≠ ∅
⊢ False
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
this : Set.Nonempty (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i)
⊢ False
rw [nonempty_iff_ne_empty] at this
no goals
α : Type u
β : Type v
ι✝ : Type ?u.21500
π : ι✝ → Type ?u.21505
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
ι : Type v
hι : Nonempty ι
Z : ι → Set α
hZd : Directed (fun x x_1 => x ⊇ x_1) Z
hZn : ∀ (i : ι), Set.Nonempty (Z i)
hZc : ∀ (i : ι), IsCompact (Z i)
hZcl : ∀ (i : ι), IsClosed (Z i)
i₀ : ι
Z' : ι → Set α := fun i => Z i ∩ Z i₀
H : (⋂ (i : ι), Z' i) = ∅
t : Finset ι
ht : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) = ∅
i₁ : ι
hi₁ : Z i₁ ⊆ Z i₀ ∧ ∀ (i : ι), i ∈ t → Z i₁ ⊆ Z' i
this : (Z i₀ ∩ ⋂ (i : ι) (_ : i ∈ t), Z' i) ≠ ∅
⊢ False
contradiction