Hom

📁 Source: Mathlib/Topology/Bornology/Hom.lean

Statistics

Metric	Count
Definitions LocallyBoundedMap, comp, copy, id, instFunLike, instInhabited, ofMapBounded, toFun, LocallyBoundedMapClass, toLocallyBoundedMap, instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass	11
Theorems image, cancel_left, cancel_right, coe_comp, coe_copy, coe_id, coe_ofMapBounded, comap_cobounded_le', comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instLocallyBoundedMapClass, ofMapBounded_apply, comap_cobounded_le	19
Total	30

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image 📖	mathematical	Bornology.IsBounded	Set.image DFunLike.coe	—	Bornology.comap_cobounded_le_iff LocallyBoundedMapClass.comap_cobounded_le

LocallyBoundedMap

Definitions

Name	Category	Theorems
comp 📖	CompOp	7 math math: id_comp, comp_assoc, coe_comp, cancel_right, comp_id, comp_apply, cancel_left
copy 📖	CompOp	2 math math: copy_eq, coe_copy
id 📖	CompOp	4 math math: id_comp, coe_id, id_apply, comp_id
instFunLike 📖	CompOp	9 math math: coe_id, instLocallyBoundedMapClass, ext_iff, coe_comp, coe_ofMapBounded, LipschitzWith.coe_toLocallyBoundedMap, id_apply, ofMapBounded_apply, comp_apply
instInhabited 📖	CompOp	—
ofMapBounded 📖	CompOp	2 math math: coe_ofMapBounded, ofMapBounded_apply
toFun 📖	CompOp	1 math math: comap_cobounded_le'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe LocallyBoundedMap instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe LocallyBoundedMap instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_comp 📖	mathematical	—	DFunLike.coe LocallyBoundedMap instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe LocallyBoundedMap instFunLike	copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe LocallyBoundedMap instFunLike id	—	—
coe_ofMapBounded 📖	mathematical	Bornology.IsBounded Set.image	DFunLike.coe LocallyBoundedMap instFunLike ofMapBounded	—	—
comap_cobounded_le' 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap toFun Bornology.cobounded	—	—
comp_apply 📖	mathematical	—	DFunLike.coe LocallyBoundedMap instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	ext
copy_eq 📖	mathematical	DFunLike.coe LocallyBoundedMap instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe LocallyBoundedMap instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe LocallyBoundedMap instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe LocallyBoundedMap instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	ext
instLocallyBoundedMapClass 📖	mathematical	—	LocallyBoundedMapClass LocallyBoundedMap instFunLike	—	comap_cobounded_le'
ofMapBounded_apply 📖	mathematical	Bornology.IsBounded Set.image	DFunLike.coe LocallyBoundedMap instFunLike ofMapBounded	—	—

LocallyBoundedMapClass

Definitions

Name	Category	Theorems
toLocallyBoundedMap 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_cobounded_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap DFunLike.coe Bornology.cobounded	—	—

(root)

Definitions

Name	Category	Theorems
LocallyBoundedMap 📖	CompData	9 math math: LocallyBoundedMap.coe_id, LocallyBoundedMap.instLocallyBoundedMapClass, LocallyBoundedMap.ext_iff, LocallyBoundedMap.coe_comp, LocallyBoundedMap.coe_ofMapBounded, LipschitzWith.coe_toLocallyBoundedMap, LocallyBoundedMap.id_apply, LocallyBoundedMap.ofMapBounded_apply, LocallyBoundedMap.comp_apply
LocallyBoundedMapClass 📖	CompData	1 math math: LocallyBoundedMap.instLocallyBoundedMapClass
instCoeTCLocallyBoundedMapOfLocallyBoundedMapClass 📖	CompOp	—

---

← Back to Index