isCompact_iff_totallyBounded_isComplete

English

IsCompact s is equivalent to TotallyBounded s together with IsComplete s.

Русский

Компактность множества эквивалентна сочетанию полной ограниченности и полноты.

LaTeX

$$$$IsCompact(s) \\iff (TotallyBounded(s) \\land IsComplete(s)).$$$$

Lean4

theorem isCompact_iff_totallyBounded_isComplete {s : Set α} : IsCompact s ↔ TotallyBounded s ∧ IsComplete s :=
  ⟨fun hs =>
    ⟨totallyBounded_iff_ultrafilter.2 fun f hf =>
        let ⟨_, _, fx⟩ := isCompact_iff_ultrafilter_le_nhds.1 hs f hf
        cauchy_nhds.mono fx,
      fun f fc fs =>
      let ⟨a, as, fa⟩ := @hs f fc.1 fs
      ⟨a, as, le_nhds_of_cauchy_adhp fc fa⟩⟩,
    fun ⟨ht, hc⟩ => isCompact_iff_ultrafilter_le_nhds.2 fun f hf => hc _ (totallyBounded_iff_ultrafilter.1 ht f hf) hf⟩

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