case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
O₁ O₂ : Set α
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
obtain ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩ :=
  isCompact_isCompact_separated (hK.diff hU) (hK.diff hV)
    (by rwa [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty])
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
O₁ O₂ : Set α
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ ∃ K₁ K₂, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂
exact
  ⟨_, _, hK.diff h1O₁, hK.diff h1O₂, by rwa [diff_subset_comm], by rwa [diff_subset_comm], by
    rw [← diff_inter, hO.inter_eq, diff_empty]⟩
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
⊢ Disjoint (K \ U) (K \ V)
rwa [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
O₁ O₂ : Set α
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K \ O₁ ⊆ U
rwa [diff_subset_comm]
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
O₁ O₂ : Set α
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K \ O₂ ⊆ V
rwa [diff_subset_comm]
no goals
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
γ : Type ?u.133233
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space α
K U V : Set α
hK : IsCompact K
hU : IsOpen U
hV : IsOpen V
h2K : K ⊆ U ∪ V
O₁ O₂ : Set α
h1O₁ : IsOpen O₁
h1O₂ : IsOpen O₂
h2O₁ : K \ U ⊆ O₁
h2O₂ : K \ V ⊆ O₂
hO : Disjoint O₁ O₂
⊢ K = K \ O₁ ∪ K \ O₂
rw [← diff_inter, hO.inter_eq, diff_empty]