isBounded_iff — Mathlib

English

In the inCompact bornology, a set s is bounded iff there exists a compact t with s ⊆ t.

Русский

В борологии inCompact множество ограничено тогда и только тогда, когда существует компактное надмножество t с s ⊆ t.

LaTeX

$$$ IsBounded_{inCompact X}(s) \\iff \\exists t\\; (IsCompact(t) \\wedge s \\subseteq t) $$$

Lean4

theorem isBounded_iff : @IsBounded _ (inCompact X) s ↔ ∃ t, IsCompact t ∧ s ⊆ t :=
  by
  change sᶜ ∈ Filter.cocompact X ↔ _
  rw [Filter.mem_cocompact]
  simp

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