α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ (s ∩ ⋂ (i : ι), Z i) ≠ ∅
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), Set.Nonempty (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i)
⊢ Set.Nonempty (s ∩ ⋂ (i : ι), Z i)
simp only [nonempty_iff_ne_empty] at hsZ⊢
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ ¬∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ (s ∩ ⋂ (i : ι), Z i) ≠ ∅
apply mt (hs.elim_finite_subfamily_closed Z hZc)
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ ¬∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
push_neg
no goals
α : Type u
β : Type v
ι✝ : Type ?u.20882
π : ι✝ → Type ?u.20887
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s : Set α
ι : Type v
hs : IsCompact s
Z : ι → Set α
hZc : ∀ (i : ι), IsClosed (Z i)
hsZ : ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
⊢ ∀ (t : Finset ι), (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) ≠ ∅
exact hsZ