boundedSpace_induced_iff — Mathlib

English

For a map f, BoundedSpace under the induced Bornology by f is equivalent to IsBounded(range f).

Русский

Для отображения f пространство ограничено в индуцированной борологии тогда и только тогда, когда множество образов range f ограничено.

LaTeX

$$$\\text{BoundedSpace}_{\\text{induced } f} \\iff \\operatorname{IsBounded}(\\operatorname{range}(f))$$$

Lean4

theorem boundedSpace_induced_iff {α β : Type*} [Bornology β] {f : α → β} :
    @BoundedSpace α (Bornology.induced f) ↔ IsBounded (range f) := by
  rw [← @isBounded_univ, isBounded_induced, image_univ]

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