exists_superset_of_isCompact — Mathlib

English

There is a minimal n such that x ∈ K_n (the find function).

Русский

Существует наименьшее n, такое что x ∈ K_n (функция find).

LaTeX

$$$$\text{find}_K(x) = \min\{n\in\mathbb{N} : x\in K_n\}.$$$$

Lean4

/-- A compact exhaustion eventually covers any compact set. -/
theorem exists_superset_of_isCompact {s : Set X} (hs : IsCompact s) : ∃ n, s ⊆ K n :=
  by
  suffices ∃ n, s ⊆ interior (K n) from this.imp fun _ ↦ (Subset.trans · interior_subset)
  refine hs.elim_directed_cover (interior ∘ K) (fun _ ↦ isOpen_interior) ?_ ?_
  · intro x _
    rcases K.exists_mem x with ⟨k, hk⟩
    exact mem_iUnion.2 ⟨k + 1, K.subset_interior_succ _ hk⟩
  · exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

Похожие утверждения