ofMapBounded — Mathlib

English

If f : α → β maps bounded sets to bounded sets, then there exists a LocallyBoundedMap α β whose underlying function is f.

Русский

Если функция f : α → β отображает ограниченные множества в ограниченные, то существует локально ограниченная отображающая функция α → β, имеющая в основе функцию f.

LaTeX

$$$\\exists F : \\operatorname{LocallyBoundedMap} \\alpha \\beta, F = \\operatorname{ofMapBounded}(f,h).$$$

Lean4

/-- Construct a `LocallyBoundedMap` from the fact that the function maps bounded sets to bounded
sets. -/
def ofMapBounded (f : α → β) (h : ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)) : LocallyBoundedMap α β :=
  ⟨f, comap_cobounded_le_iff.2 h⟩

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