isBounded_iff — Mathlib

English

For any subset s of α, s is bounded if and only if there exists a constant C such that for all x ∈ s and all y ∈ s, dist x y ≤ C.

Русский

Для любого подмножества s пространства α: s ограничено тогда и только тогда, когда существует C such что для всех x ∈ s и y ∈ s, dist x y ≤ C.

LaTeX

$$$ IsBounded(s) \iff \exists C \in \mathbb{R}, \forall x \in s, \forall y \in s, dist(x,y) \le C $$$

Lean4

theorem isBounded_iff {s : Set α} : IsBounded s ↔ ∃ C : ℝ, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C := by
  rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq, compl_compl]

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