English
Given a neighborhood of the diagonal in X×X, there exists a finite open cover of X×X by opens Ui such that Ui×Ui ⊆ S for all i.
Русский
Для окрестности диагонали в X×X существует конечное открытое покрытие X×X такими открытыми множествами Ui, что Ui×Ui ⊆ S для всех i.
LaTeX
$$$\exists t: Finset X, U: t \to Opens X, \; IsOpenCover U \land \forall i, (U_i : Set X) \times^s U_i ⊆ S$$$
Lean4
/-- If `S` is any neighbourhood of the diagonal in a compact topological space `X`, then there
exists a finite cover of `X` by opens `U i` such that `U i ×ˢ U i ⊆ S` for all `i`.
That the indexing set is a finset of `X` is an artifact of the proof; it could be any finite type.
-/
theorem exists_finite_open_cover_prod_subset_of_mem_nhds_diagonal_of_compact (hS : S ∈ nhdsSet (diagonal X)) :
∃ (t : Finset X) (U : t → Opens X), IsOpenCover U ∧ ∀ i, (U i : Set X) ×ˢ U i ⊆ S :=
by
choose U hUo hUx hUp using exists_open_prod_subset_of_mem_nhds_diagonal hS
obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover _ hUo (fun x _ ↦ mem_iUnion.mpr ⟨_, hUx x⟩)
refine ⟨t, fun i ↦ ⟨_, hUo i⟩, .of_sets _ ?_, (hUp ·)⟩
simpa [iUnion_subtype, ← univ_subset_iff] using ht
