isBounded_iff_forall_mem — Mathlib

English

IsBounded s if and only if every element of s is contained in a bounded set, i.e., IsBounded s for all x ∈ s.

Русский

IsBounded s эквивалентно тому, что каждый элемент s содержится в ограниченном множестве.

LaTeX

$$$IsBounded s \\iff \\forall x \\in s,\\ IsBounded s$$$

Lean4

theorem isBounded_iff_forall_mem : IsBounded s ↔ ∀ x ∈ s, IsBounded s :=
  ⟨fun h _ _ ↦ h, fun h ↦ by
    rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
    exacts [isBounded_empty, h x hx]⟩

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