Theorems · Theorem · general topology

LocallyBoundedMap.ofMapBounded_apply

∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] (f : α → β)
  {h : ∀ ⦃s : Set α⦄, Bornology.IsBounded s → Bornology.IsBounded (f '' s)} (a : α),
  (LocallyBoundedMap.ofMapBounded f h) a = f a

Defined in

Mathlib.Topology.Bornology.Hom

Cited by

0 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

BornologyBornology