Theorems · Inductive type · general topology

LocallyBoundedMap

(α : Type u_6) → (β : Type u_7) → [Bornology α] → [Bornology β] → Type (max u_6 u_7)

The type of bounded maps from α to β, the maps which send a bounded set to a bounded set.

Defined in

Mathlib.Topology.Bornology.Hom

Cited by

20 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

BornologyBornology