isBounded_ofBounded_iff — Mathlib

English

Under the same B, IsBounded of s in the resulting Bornology ofBounded B equals membership of s in B.

Русский

При той же структуре B ограниченность поднастройки равна принадлежности s к B.

LaTeX

$$$\big(IsBounded\,(ofBounded\ B\empty_mem\subset_mem\union_mem\sUnion_univ)\, s) \iff s \in B$$$

Lean4

theorem isBounded_ofBounded_iff (B : Set (Set α)) {empty_mem subset_mem union_mem sUnion_univ} :
    @IsBounded _ (ofBounded B empty_mem subset_mem union_mem sUnion_univ) s ↔ s ∈ B := by
  rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]

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