α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
refine' ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => _⟩
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hxU : ∀ (x : α), x ∈ s → x ∈ U x ∧ IsOpen (U x)
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l
choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
⊢ Disjoint (𝓝ˢ s) l
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hxU : ∀ (x : α), x ∈ s → x ∈ U x ∧ IsOpen (U x)
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
⊢ Disjoint (𝓝ˢ s) l
choose hxU hUo using hxU
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ Disjoint (𝓝ˢ s) l
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
⊢ Disjoint (𝓝ˢ s) l
rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ (⋃ (x : α) (_ : x ∈ t), U x)ᶜ ∈ l
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ Disjoint (𝓝ˢ s) l
refine'
  (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, _⟩
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ ∀ (i : α), i ∈ t → U iᶜ ∈ l
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ (⋃ (x : α) (_ : x ∈ t), U x)ᶜ ∈ l
rw [compl_iUnion₂, biInter_finset_mem]
no goals
case intro.intro
α : Type u
β : Type v
ι : Type ?u.16218
π : ι → Type ?u.16223
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t✝ : Set α
l : Filter α
hs : IsCompact s
H : ∀ (x : α), x ∈ s → Disjoint (𝓝 x) l
U : α → Set α
hUl : ∀ (x : α), x ∈ s → U xᶜ ∈ l
hxU : ∀ (x : α), x ∈ s → x ∈ U x
hUo : ∀ (x : α), x ∈ s → IsOpen (U x)
t : Finset α
hts : ∀ (x : α), x ∈ t → x ∈ s
hst : s ⊆ ⋃ (x : α) (_ : x ∈ t), U x
⊢ ∀ (i : α), i ∈ t → U iᶜ ∈ l
exact fun x hx => hUl x (hts x hx)