Bornology

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

Statistics

Metric	Count
Definitions Bornology, IsOrderBornology, orderBornology	3
Theorems isBounded, isBounded_inter, isBounded, isBounded_inter, bddAbove, bddBelow, subset_Icc_sInf_sSup, isBounded_iff_bddBelow_bddAbove, instIsOrderBornology, instIsOrderBornology, instIsOrderBornology, isBounded_iff_bddBelow_bddAbove, isOrderBornology_iff_eq_orderBornology, orderBornology_isBounded	14
Total	17

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded 📖	mathematical	BddAbove Preorder.toLE BddBelow	Bornology.IsBounded	—	isBounded_iff_bddBelow_bddAbove
isBounded_inter 📖	mathematical	BddAbove Preorder.toLE BddBelow	Bornology.IsBounded Set Set.instInter	—	isBounded mono Set.inter_subset_left BddBelow.mono Set.inter_subset_right

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded 📖	mathematical	BddBelow Preorder.toLE BddAbove	Bornology.IsBounded	—	isBounded_iff_bddBelow_bddAbove
isBounded_inter 📖	mathematical	BddBelow Preorder.toLE BddAbove	Bornology.IsBounded Set Set.instInter	—	isBounded mono Set.inter_subset_left BddAbove.mono Set.inter_subset_right

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove 📖	mathematical	Bornology.IsBounded	BddAbove Preorder.toLE	—	isBounded_iff_bddBelow_bddAbove
bddBelow 📖	mathematical	Bornology.IsBounded	BddBelow Preorder.toLE	—	isBounded_iff_bddBelow_bddAbove
subset_Icc_sInf_sSup 📖	mathematical	Bornology.IsBounded	Set Set.instHasSubset Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet	—	subset_Icc_csInf_csSup bddBelow bddAbove

IsOrderBornology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_iff_bddBelow_bddAbove 📖	mathematical	—	Bornology.IsBounded BddBelow Preorder.toLE BddAbove	—	—

OrderDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderBornology 📖	mathematical	—	IsOrderBornology OrderDual instBornologyOrderDual instPreorder	—	isBounded_preimage_toDual bddBelow_preimage_toDual bddAbove_preimage_toDual isBounded_iff_bddBelow_bddAbove

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderBornology 📖	mathematical	IsOrderBornology	instBornology preorder	—	—

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderBornology 📖	mathematical	—	IsOrderBornology instBornology instPreorder	—	Bornology.isBounded_image_fst_and_snd bddBelow_prod bddAbove_prod isBounded_iff_bddBelow_bddAbove

(root)

Definitions

Name	Category	Theorems
Bornology 📖	CompData	—
IsOrderBornology 📖	CompData	8 math math: Real.instIsOrderBornology, Prod.instIsOrderBornology, NNReal.instIsOrderBornology, OrderDual.instIsOrderBornology, IsOrderBornology.of_isCompactIcc, Nat.instIsOrderBornology, isOrderBornology_iff_eq_orderBornology, Int.instIsOrderBornology
orderBornology 📖	CompOp	2 math math: orderBornology_isBounded, isOrderBornology_iff_eq_orderBornology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_iff_bddBelow_bddAbove 📖	mathematical	—	Bornology.IsBounded BddBelow Preorder.toLE BddAbove	—	IsOrderBornology.isBounded_iff_bddBelow_bddAbove
isOrderBornology_iff_eq_orderBornology 📖	mathematical	—	IsOrderBornology PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf orderBornology	—	Bornology.ext Filter.ext Bornology.isBounded_compl_iff IsOrderBornology.isBounded_iff_bddBelow_bddAbove orderBornology_isBounded
orderBornology_isBounded 📖	mathematical	—	Bornology.IsBounded orderBornology BddBelow Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf BddAbove	—	compl_compl

---

← Back to Index