α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊆ ⋃ (i : ι✝), U i
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
case intro
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
t : Finset ι✝
ht : (s ∩ ⋂ (i : ι✝) (_ : i ∈ t), U iᶜ) = ∅
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
case intro
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
t : Finset ι✝
ht : (s ∩ ⋂ (i : ι✝) (_ : i ∈ t), U iᶜ) = ∅
⊢ s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
case intro
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
t : Finset ι✝
ht : (s ∩ ⋂ (i : ι✝) (_ : i ∈ t), U iᶜ) = ∅
⊢ ∃ t, s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
refine ⟨t, ?_⟩
no goals
case intro
α : Type u
β : Type v
ι : Type ?u.27539
π : ι → Type ?u.27544
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
h :
  ∀ {ι : Type u} (Z : ι → Set α),
    (∀ (i : ι), IsClosed (Z i)) → (s ∩ ⋂ (i : ι), Z i) = ∅ → ∃ t, (s ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
ι✝ : Type u
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : (s ⊓ ⋂ (i : ι✝), U iᶜ) = ⊥
t : Finset ι✝
ht : (s ∩ ⋂ (i : ι✝) (_ : i ∈ t), U iᶜ) = ∅
⊢ s ⊆ ⋃ (i : ι✝) (_ : i ∈ t), U i
rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]