English
If a compact set K is covered by two open sets U and V, then there exist compact K1 ⊆ U and K2 ⊆ V such that K = K1 ∪ K2.
Русский
Если компактное K покрыто двумя открытыми множествами U и V, то существуют компактные K1 ⊆ U и K2 ⊆ V такие, что K = K1 ∪ K2.
LaTeX
$$∃ K1 K2, IsCompact(K1) ∧ IsCompact(K2) ∧ K1 ⊆ U ∧ K2 ⊆ V ∧ K = K1 ∪ K2$$
Lean4
/-- If a compact set is covered by two open sets, then we can cover it by two compact subsets. -/
theorem binary_compact_cover {K U V : Set X} (hK : IsCompact K) (hU : IsOpen U) (hV : IsOpen V) (h2K : K ⊆ U ∪ V) :
∃ K₁ K₂ : Set X, IsCompact K₁ ∧ IsCompact K₂ ∧ K₁ ⊆ U ∧ K₂ ⊆ V ∧ K = K₁ ∪ K₂ :=
by
have hK' : IsCompact (closure K) := hK.closure
have : SeparatedNhds (closure K \ U) (closure K \ V) :=
by
apply SeparatedNhds.of_isCompact_isCompact_isClosed (hK'.diff hU) (hK'.diff hV) (isClosed_closure.sdiff hV)
rw [disjoint_iff_inter_eq_empty, diff_inter_diff, diff_eq_empty]
exact hK.closure_subset_of_isOpen (hU.union hV) h2K
have : SeparatedNhds (K \ U) (K \ V) :=
this.mono (diff_subset_diff_left (subset_closure)) (diff_subset_diff_left (subset_closure))
rcases this with ⟨O₁, O₂, h1O₁, h1O₂, h2O₁, h2O₂, hO⟩
exact
⟨K \ O₁, K \ O₂, hK.diff h1O₁, hK.diff h1O₂, diff_subset_comm.mp h2O₁, diff_subset_comm.mp h2O₂, by
rw [← diff_inter, hO.inter_eq, diff_empty]⟩
