Bounded

📁 Source: Mathlib/Topology/MetricSpace/Bounded.lean

Statistics

Metric	Count
Definitions evalDiam, diam, Bounded, Bounded	4
Theorems closure, ediam_ne_top, isCompact_closure, subset_ball, subset_ball_lt, subset_closedBall, subset_closedBall_lt, closedBall_compl_subset, isBounded_range, exists_forall_ge_of_isBounded, exists_forall_le_of_isBounded, isBounded, nonempty_iInter_of_nonempty_biInter, of_isCompactIcc, closedBall_compl_subset_of_mem_cocompact, cobounded_eq_cocompact, cobounded_le_cocompact, comap_dist_left_atTop, comap_dist_right_atTop, compactSpace_iff_isBounded_univ, diam_ball, diam_closedBall, diam_empty, diam_eq_zero_of_unbounded, diam_le_of_forall_dist_le, diam_le_of_forall_dist_le_of_nonempty, diam_le_of_subset_closedBall, diam_mono, diam_nonneg, diam_one, diam_pair, diam_pos, diam_singleton, diam_subsingleton, diam_triple, diam_union, diam_union', diam_univ_of_noncompact, diam_zero, disjoint_cobounded_nhds, disjoint_cobounded_nhdsSet, disjoint_nhdsSet_cobounded, disjoint_nhds_cobounded, dist_le_diam_of_mem, dist_le_diam_of_mem', ediam_eq_top_iff_unbounded, ediam_le_of_forall_dist_le, ediam_of_unbounded, ediam_univ_eq_top_iff_noncompact, ediam_univ_of_noncompact, exists_isBounded_image_of_tendsto, exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn, exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt, exists_isOpen_isBounded_image_of_isCompact_of_continuousOn, exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt, finite_isBounded_inter_isClosed, hasAntitoneBasis_cobounded_compl_ball, hasAntitoneBasis_cobounded_compl_closedBall, hasBasis_cobounded_compl_ball, hasBasis_cobounded_compl_closedBall, isBounded_Icc, isBounded_Ico, isBounded_Ioc, isBounded_Ioo, isBounded_ball, isBounded_closedBall, isBounded_closure_iff, isBounded_closure_of_isBounded, isBounded_iff_ediam_ne_top, isBounded_iff_subset_ball, isBounded_iff_subset_closedBall, isBounded_image_iff, isBounded_of_abs_le, isBounded_of_abs_lt, isBounded_of_bddAbove_of_bddBelow, isBounded_of_compactSpace, isBounded_range_iff, isBounded_range_of_cauchy_map_cofinite, isBounded_range_of_tendsto, isBounded_range_of_tendsto_cofinite, isBounded_range_of_tendsto_cofinite_uniformity, isBounded_sphere, isCobounded_iff_closedBall_compl_subset, isCompact_iff_isClosed_bounded, isCompact_of_isClosed_isBounded, mem_cocompact_iff_closedBall_compl_subset, mem_cocompact_of_closedBall_compl_subset, nonempty_iInter_of_nonempty_biInter, tendsto_dist_left_atTop_iff, tendsto_dist_left_cobounded_atTop, tendsto_dist_right_atTop_iff, tendsto_dist_right_cobounded_atTop, isBounded, comap_dist_left_atTop_eq_cocompact, tendsto_cocompact_of_tendsto_dist_comp_atTop, tendsto_dist_left_cocompact_atTop, tendsto_dist_right_cocompact_atTop, totallyBounded_Icc, totallyBounded_Ico, totallyBounded_Ioc, totallyBounded_Ioo	101
Total	105

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Metric.isBounded_closure_of_isBounded
ediam_ne_top 📖	—	Bornology.IsBounded PseudoMetricSpace.toBornology	—	—	Metric.isBounded_iff_ediam_ne_top
isCompact_closure 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace closure	—	Metric.isCompact_of_isClosed_isBounded isClosed_closure closure
subset_ball 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	Set Set.instHasSubset Metric.ball	—	subset_ball_lt
subset_ball_lt 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	Real Real.instLT Set Set.instHasSubset Metric.ball	—	subset_closedBall LE.le.trans_lt le_max_right lt_add_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid HasSubset.Subset.trans Set.instIsTransSubset Metric.closedBall_subset_ball le_max_left
subset_closedBall 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	Set Set.instHasSubset Metric.closedBall	—	Metric.isBounded_iff_subset_closedBall
subset_closedBall_lt 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	Real Real.instLT Set Set.instHasSubset Metric.closedBall	—	subset_ball_lt HasSubset.Subset.trans Set.instIsTransSubset Metric.ball_subset_closedBall

Bornology.IsCobounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedBall_compl_subset 📖	mathematical	Bornology.IsCobounded PseudoMetricSpace.toBornology	Set Set.instHasSubset Compl.compl Set.instCompl Metric.closedBall	—	Metric.isCobounded_iff_closedBall_compl_subset

CauchySeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_range 📖	mathematical	CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	Metric.isBounded_range_of_cauchy_map_cofinite Nat.cofinite_eq_atTop

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_forall_ge_of_isBounded 📖	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.IsBounded PseudoMetricSpace.toBornology setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	exists_forall_le_of_isBounded instOrderClosedTopologyOrderDual
exists_forall_le_of_isBounded 📖	—	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.IsBounded PseudoMetricSpace.toBornology setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	—	exists_forall_le' instClosedIicTopology Filter.mem_cocompact' Metric.isCompact_of_isClosed_isBounded isClosed_le continuous_const Filter.mp_mem Filter.univ_mem' LT.lt.le

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology	—	TotallyBounded.isBounded totallyBounded

IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nonempty_iInter_of_nonempty_biInter 📖	—	IsComplete PseudoMetricSpace.toUniformSpace IsClosed UniformSpace.toTopologicalSpace Bornology.IsBounded PseudoMetricSpace.toBornology Set.Nonempty Set.iInter Filter.Tendsto Real Metric.diam Filter.atTop Nat.instPreorder nhds Real.pseudoMetricSpace Real.instZero	—	—	Set.mem_of_subset_of_mem cauchySeq_of_le_tendsto_0 Metric.dist_le_diam_of_mem cauchySeq_tendsto_of_isComplete zero_le Nat.instCanonicallyOrderedAdd Set.mem_iInter IsClosed.mem_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.mp_mem Filter.Ici_mem_atTop Filter.univ_mem'

IsOrderBornology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isCompactIcc 📖	mathematical	BddBelow Preorder.toLE Metric.closedBall BddAbove	IsOrderBornology PseudoMetricSpace.toBornology	—	Metric.isBounded_iff_subset_closedBall BddBelow.mono BddAbove.mono Metric.isBounded_of_bddAbove_of_bddBelow

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalDiam 📖	CompOp	—

Metric

Definitions

Name	Category	Theorems
diam 📖	CompOp	64 math math: IsometryClass.diam_image, LinearIsometry.diam_image, diam_mono, diam_triple, diam_smul₀, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, diam_closure, diam_le_of_subset_closedBall, IsometryEquiv.diam_image, convexHull_diam, diam_eq_zero_of_unbounded, diam_stdSimplex, diam_closedBall_eq, Isometry.diam_range, IsometryClass.diam_range, LinearIsometryEquiv.diam_image, Real.diam_Ioo, dist_le_infDist_add_diam, diam_thickening_le, AffineIsometry.diam_image, diam_stdSimplex_of_subsingleton, diam_ball, diam_nonneg, diam_closedBall, diam_stdSimplex_le, AffineIsometryEquiv.diam_image, Real.diam_eq, hausdorffDist_le_diam, diam_ball_eq, diam_pair, diam_smul, dist_le_diam_of_mem, IsometryEquiv.diam_preimage, diam_singleton, BoxIntegral.Box.diam_Icc_le_of_distortion_le, AffineIsometry.diam_range, LinearIsometry.diam_range, BoxIntegral.TaggedPrepartition.IsSubordinate.diam_le, diam_sphere_eq, diam_le_of_forall_dist_le_of_nonempty, Isometry.diam_image, diam_union', diam_vadd, Dilation.diam_range, Dilation.diam_image, diam_pos, Real.diam_Ico, diam_subsingleton, SemilinearIsometryClass.diam_image, diam_empty, dist_le_diam_of_mem', diam_zero, diam_one, IsometryEquiv.diam_univ, BoxIntegral.unitPartition.diam_boxIcc, LipschitzWith.diam_image_le, Real.diam_Ioc, SemilinearIsometryClass.diam_range, diam_le_of_forall_dist_le, diam_union, diam_cthickening_le, diam_univ_of_noncompact, Real.diam_Icc, GromovHausdorff.HD_candidatesBDist_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedBall_compl_subset_of_mem_cocompact 📖	mathematical	Set Filter Filter.instMembership Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set.instHasSubset Compl.compl Set.instCompl closedBall	—	Bornology.IsCobounded.closedBall_compl_subset cobounded_le_cocompact
cobounded_eq_cocompact 📖	mathematical	—	Bornology.cobounded PseudoMetricSpace.toBornology Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Bornology.cobounded_eq_bot BoundedSpace.of_finite Finite.of_subsingleton Filter.cocompact_eq_bot Finite.compactSpace LE.le.antisymm cobounded_le_cocompact Nontrivial.to_nonempty Filter.HasBasis.ge_iff hasBasis_cobounded_compl_closedBall IsCompact.compl_mem_cocompact ProperSpace.isCompact_closedBall
cobounded_le_cocompact 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Bornology.cobounded PseudoMetricSpace.toBornology Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Filter.HasBasis.ge_iff Filter.hasBasis_cocompact IsCompact.isBounded
comap_dist_left_atTop 📖	mathematical	—	Filter.comap Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology	—	dist_comm comap_dist_right_atTop
comap_dist_right_atTop 📖	mathematical	—	Filter.comap Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology	—	Filter.HasBasis.eq_of_same_basis Filter.HasBasis.comap Filter.atTop_basis instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean hasBasis_cobounded_compl_ball
compactSpace_iff_isBounded_univ 📖	mathematical	—	CompactSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.IsBounded PseudoMetricSpace.toBornology Set.univ	—	isBounded_of_compactSpace isCompact_of_isClosed_isBounded isClosed_univ
diam_ball 📖	mathematical	Real Real.instLE Real.instZero	diam ball Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	diam_le_of_subset_closedBall ball_subset_closedBall
diam_closedBall 📖	mathematical	Real Real.instLE Real.instZero	diam closedBall Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	diam_le_of_subset_closedBall Set.Subset.rfl
diam_empty 📖	mathematical	—	diam Set Set.instEmptyCollection Real Real.instZero	—	diam_subsingleton Set.subsingleton_empty
diam_eq_zero_of_unbounded 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	diam Real Real.instZero	—	diam.eq_1 ediam_of_unbounded ENNReal.toReal_top
diam_le_of_forall_dist_le 📖	mathematical	Real Real.instLE Real.instZero Dist.dist PseudoMetricSpace.toDist	diam	—	ENNReal.toReal_le_of_le_ofReal ediam_le_of_forall_dist_le
diam_le_of_forall_dist_le_of_nonempty 📖	mathematical	Set.Nonempty Real Real.instLE Dist.dist PseudoMetricSpace.toDist	diam	—	le_trans dist_nonneg diam_le_of_forall_dist_le
diam_le_of_subset_closedBall 📖	mathematical	Real Real.instLE Real.instZero Set Set.instHasSubset closedBall	diam Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	diam_le_of_forall_dist_le Nat.instAtLeastTwoHAddOfNat mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing zero_le_two Real.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid dist_triangle_right add_le_add covariant_swap_add_of_covariant_add mul_comm mul_two
diam_mono 📖	mathematical	Set Set.instHasSubset Bornology.IsBounded PseudoMetricSpace.toBornology	Real Real.instLE diam	—	ENNReal.toReal_mono Bornology.IsBounded.ediam_ne_top ediam_mono
diam_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero diam	—	ENNReal.toReal_nonneg
diam_one 📖	mathematical	—	diam Set Set.one Real Real.instZero	—	diam_singleton
diam_pair 📖	mathematical	—	diam Set Set.instInsert Set.instSingletonSet Dist.dist PseudoMetricSpace.toDist	—	ediam_pair dist_edist
diam_pos 📖	mathematical	Set.Nontrivial Bornology.IsBounded PseudoMetricSpace.toBornology MetricSpace.toPseudoMetricSpace	Real Real.instLT Real.instZero diam	—	LT.lt.trans_le dist_pos dist_le_diam_of_mem
diam_singleton 📖	mathematical	—	diam Set Set.instSingletonSet Real Real.instZero	—	diam_subsingleton Set.subsingleton_singleton
diam_subsingleton 📖	mathematical	Set.Subsingleton	diam Real Real.instZero	—	ediam_subsingleton
diam_triple 📖	mathematical	—	diam Set Set.instInsert Set.instSingletonSet Real Real.instMax Dist.dist PseudoMetricSpace.toDist	—	ediam_triple dist_edist ENNReal.toReal_max ne_of_lt max_lt edist_lt_top
diam_union 📖	mathematical	Set Set.instMembership	Real Real.instLE diam Set.instUnion Real.instAdd Dist.dist PseudoMetricSpace.toDist	—	dist_edist le_imp_le_of_le_of_le ENNReal.toReal_le_add' ediam_union_le_add_edist top_unique ediam_mono Set.subset_union_left Set.subset_union_right le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.toReal_add_le
diam_union' 📖	mathematical	Set.Nonempty Set Set.instInter	Real Real.instLE diam Set.instUnion Real.instAdd	—	dist_self add_zero diam_union
diam_univ_of_noncompact 📖	mathematical	—	diam Set.univ Real Real.instZero	—	ediam_univ_of_noncompact
diam_zero 📖	mathematical	—	diam Set Set.zero Real Real.instZero	—	diam_singleton
disjoint_cobounded_nhds 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Bornology.cobounded PseudoMetricSpace.toBornology nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Disjoint.symm disjoint_nhds_cobounded
disjoint_cobounded_nhdsSet 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Bornology.cobounded PseudoMetricSpace.toBornology nhdsSet	—	Disjoint.symm disjoint_nhdsSet_cobounded
disjoint_nhdsSet_cobounded 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhdsSet Bornology.cobounded PseudoMetricSpace.toBornology	—	IsCompact.disjoint_nhdsSet_left disjoint_nhds_cobounded
disjoint_nhds_cobounded 📖	mathematical	—	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.cobounded PseudoMetricSpace.toBornology	—	Filter.disjoint_of_disjoint_of_mem disjoint_compl_right ball_mem_nhds one_pos Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing isBounded_ball
dist_le_diam_of_mem 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology Set Set.instMembership	Real Real.instLE Dist.dist PseudoMetricSpace.toDist diam	—	dist_le_diam_of_mem' Bornology.IsBounded.ediam_ne_top
dist_le_diam_of_mem' 📖	mathematical	Set Set.instMembership	Real Real.instLE Dist.dist PseudoMetricSpace.toDist diam	—	diam.eq_1 dist_edist ENNReal.toReal_mono edist_le_ediam_of_mem
ediam_eq_top_iff_unbounded 📖	mathematical	—	ediam PseudoMetricSpace.toPseudoEMetricSpace Top.top ENNReal instTopENNReal Bornology.IsBounded PseudoMetricSpace.toBornology	—	Iff.not_left isBounded_iff_ediam_ne_top
ediam_le_of_forall_dist_le 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ediam PseudoMetricSpace.toPseudoEMetricSpace ENNReal.ofReal	—	ediam_le ENNReal.ofReal_le_ofReal edist_dist
ediam_of_unbounded 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	ediam PseudoMetricSpace.toPseudoEMetricSpace Top.top ENNReal instTopENNReal	—	ediam_eq_top_iff_unbounded
ediam_univ_eq_top_iff_noncompact 📖	mathematical	—	ediam PseudoMetricSpace.toPseudoEMetricSpace Set.univ Top.top ENNReal instTopENNReal NoncompactSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	not_compactSpace_iff compactSpace_iff_isBounded_univ isBounded_iff_ediam_ne_top
ediam_univ_of_noncompact 📖	mathematical	—	ediam PseudoMetricSpace.toPseudoEMetricSpace Set.univ Top.top ENNReal instTopENNReal	—	ediam_univ_eq_top_iff_noncompact
exists_isBounded_image_of_tendsto 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set Filter Filter.instMembership Bornology.IsBounded PseudoMetricSpace.toBornology Set.image	—	Filter.HasBasis.disjoint_iff_left Filter.HasBasis.map Filter.basis_sets Disjoint.mono_left disjoint_nhds_cobounded
exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn 📖	mathematical	IsCompact Set Set.instHasSubset ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	IsOpen Bornology.IsBounded PseudoMetricSpace.toBornology Set.image Set.instInter	—	exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt 📖	mathematical	IsCompact ContinuousWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set Set.instHasSubset IsOpen Bornology.IsBounded PseudoMetricSpace.toBornology Set.image Set.instInter	—	disjoint_assoc inf_comm IsCompact.disjoint_nhdsSet_left disjoint_left_comm Filter.Tendsto.disjoint Filter.tendsto_comap disjoint_cobounded_nhds Filter.HasBasis.disjoint_iff Filter.HasBasis.inf_principal hasBasis_nhdsSet Filter.HasBasis.comap Filter.basis_sets Bornology.IsBounded.subset Bornology.isBounded_compl_iff Set.image_subset_iff Set.preimage_compl Set.subset_compl_iff_disjoint_right
exists_isOpen_isBounded_image_of_isCompact_of_continuousOn 📖	mathematical	IsCompact IsOpen Set Set.instHasSubset ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology Set.image	—	exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt ContinuousOn.continuousAt IsOpen.mem_nhds
exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt 📖	mathematical	IsCompact ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Set Set.instHasSubset IsOpen Bornology.IsBounded PseudoMetricSpace.toBornology Set.image	—	Set.inter_univ exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
finite_isBounded_inter_isClosed 📖	mathematical	IsDiscrete UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.IsBounded PseudoMetricSpace.toBornology	Set.Finite Set Set.instInter	—	Set.Finite.subset IsCompact.finite IsCompact.inter_right Bornology.IsBounded.isCompact_closure IsDiscrete.mono Set.inter_subset_right Set.inter_subset_inter_left subset_closure
hasAntitoneBasis_cobounded_compl_ball 📖	mathematical	—	Filter.HasAntitoneBasis Real Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology Compl.compl Set Set.instCompl ball	—	hasBasis_cobounded_compl_ball LE.le.trans
hasAntitoneBasis_cobounded_compl_closedBall 📖	mathematical	—	Filter.HasAntitoneBasis Real Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology Compl.compl Set Set.instCompl closedBall	—	hasBasis_cobounded_compl_closedBall LE.le.trans_lt
hasBasis_cobounded_compl_ball 📖	mathematical	—	Filter.HasBasis Real Bornology.cobounded PseudoMetricSpace.toBornology Compl.compl Set Set.instCompl ball	—	Function.Surjective.forall compl_surjective isBounded_iff_subset_ball
hasBasis_cobounded_compl_closedBall 📖	mathematical	—	Filter.HasBasis Real Bornology.cobounded PseudoMetricSpace.toBornology Compl.compl Set Set.instCompl closedBall	—	Function.Surjective.forall compl_surjective isBounded_iff_subset_closedBall
isBounded_Icc 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.Icc	—	TotallyBounded.isBounded totallyBounded_Icc
isBounded_Ico 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.Ico	—	TotallyBounded.isBounded totallyBounded_Ico
isBounded_Ioc 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.Ioc	—	TotallyBounded.isBounded totallyBounded_Ioc
isBounded_Ioo 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.Ioo	—	TotallyBounded.isBounded totallyBounded_Ioo
isBounded_ball 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology ball	—	Bornology.IsBounded.subset isBounded_closedBall ball_subset_closedBall
isBounded_closedBall 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology closedBall	—	isBounded_iff dist_triangle_right add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
isBounded_closure_iff 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Bornology.IsBounded.subset subset_closure Bornology.IsBounded.closure
isBounded_closure_of_isBounded 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	isBounded_iff IsClosed.closure_subset isClosed_Iic instClosedIicTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal map_mem_closure₂ continuous_dist
isBounded_iff_ediam_ne_top 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology	—	isBounded_iff ne_top_of_le_ne_top ENNReal.ofReal_ne_top ediam_le_of_forall_dist_le dist_le_diam_of_mem'
isBounded_iff_subset_ball 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set Set.instHasSubset ball	—	Bornology.IsBounded.subset_ball Bornology.IsBounded.subset isBounded_ball
isBounded_iff_subset_closedBall 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set Set.instHasSubset closedBall	—	Set.mem_insert isBounded_iff Bornology.IsBounded.insert Bornology.IsBounded.subset isBounded_closedBall
isBounded_image_iff 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.image Real Real.instLE Dist.dist PseudoMetricSpace.toDist	—	isBounded_iff
isBounded_of_abs_le 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology setOf Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup	—	Set.ext isBounded_Icc
isBounded_of_abs_lt 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology setOf Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup	—	Set.ext IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add isBounded_Ioo
isBounded_of_bddAbove_of_bddBelow 📖	mathematical	BddAbove Preorder.toLE BddBelow	Bornology.IsBounded PseudoMetricSpace.toBornology	—	Bornology.IsBounded.subset isBounded_Icc Set.mem_Icc
isBounded_of_compactSpace 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology	—	Bornology.IsBounded.subset IsCompact.isBounded isCompact_univ Set.subset_univ
isBounded_range_iff 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range Real Real.instLE Dist.dist PseudoMetricSpace.toDist	—	isBounded_iff
isBounded_range_of_cauchy_map_cofinite 📖	mathematical	Cauchy PseudoMetricSpace.toUniformSpace Filter.map Filter.cofinite	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	isBounded_range_of_tendsto_cofinite_uniformity cauchy_map_iff
isBounded_range_of_tendsto 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	CauchySeq.isBounded_range Filter.Tendsto.cauchySeq
isBounded_range_of_tendsto_cofinite 📖	mathematical	Filter.Tendsto Filter.cofinite nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	isBounded_range_of_tendsto_cofinite_uniformity Filter.Tendsto.mono_right Filter.Tendsto.prodMap Eq.trans_le nhds_prod_eq nhds_le_uniformity
isBounded_range_of_tendsto_cofinite_uniformity 📖	mathematical	Filter.Tendsto SProd.sprod Filter Filter.instSProd Filter.cofinite uniformity PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology Set.range	—	Filter.HasBasis.tendsto_iff Filter.HasBasis.prod_self Filter.hasBasis_cofinite uniformity_basis_dist zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Set.image_union_image_compl_eq_range Bornology.IsBounded.union Set.Finite.isBounded Set.Finite.image isBounded_image_iff le_of_lt
isBounded_sphere 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology sphere	—	Bornology.IsBounded.subset isBounded_closedBall sphere_subset_closedBall
isCobounded_iff_closedBall_compl_subset 📖	mathematical	—	Bornology.IsCobounded PseudoMetricSpace.toBornology Set Set.instHasSubset Compl.compl Set.instCompl closedBall	—	Bornology.isBounded_compl_iff isBounded_iff_subset_closedBall Set.compl_subset_comm
isCompact_iff_isClosed_bounded 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsClosed Bornology.IsBounded PseudoMetricSpace.toBornology	—	IsCompact.isClosed IsCompact.isBounded isCompact_of_isClosed_isBounded
isCompact_of_isClosed_isBounded 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Set.eq_empty_or_nonempty isCompact_empty Bornology.IsBounded.subset_closedBall IsCompact.of_isClosed_subset ProperSpace.isCompact_closedBall
mem_cocompact_iff_closedBall_compl_subset 📖	mathematical	—	Set Filter Filter.instMembership Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Set.instHasSubset Compl.compl Set.instCompl closedBall	—	closedBall_compl_subset_of_mem_cocompact mem_cocompact_of_closedBall_compl_subset
mem_cocompact_of_closedBall_compl_subset 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl closedBall	Filter Filter.instMembership Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Filter.mem_cocompact ProperSpace.isCompact_closedBall
nonempty_iInter_of_nonempty_biInter 📖	—	IsClosed UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Bornology.IsBounded PseudoMetricSpace.toBornology Set.Nonempty Set.iInter Filter.Tendsto Real diam Filter.atTop Nat.instPreorder nhds Real.pseudoMetricSpace Real.instZero	—	—	IsComplete.nonempty_iInter_of_nonempty_biInter IsClosed.isComplete
tendsto_dist_left_atTop_iff 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology	—	dist_comm
tendsto_dist_left_cobounded_atTop 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Bornology.cobounded PseudoMetricSpace.toBornology Filter.atTop Real.instPreorder	—	Filter.tendsto_iff_comap Eq.ge comap_dist_left_atTop
tendsto_dist_right_atTop_iff 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology	—	comap_dist_right_atTop Filter.tendsto_comap_iff
tendsto_dist_right_cobounded_atTop 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Bornology.cobounded PseudoMetricSpace.toBornology Filter.atTop Real.instPreorder	—	Filter.tendsto_iff_comap Eq.ge comap_dist_right_atTop

Ordnode

Definitions

Name	Category	Theorems
Bounded 📖	MathDef	2 math math: Valid'.ord, Bounded.dual_iff

Set

Definitions

Name	Category	Theorems
Bounded 📖	MathDef	45 math math: bounded_ge_Ioc, bounded_lt_Iio, bounded_le_Ioc, bounded_gt_Ioi, bounded_gt_inter_ge, Cardinal.mk_bounded_subset, bounded_ge_inter_not_ge, bounded_lt_inter_not_lt, bounded_le_inter_not_le, bounded_gt_Ioo, Ordinal.lt_cof_type, Ordinal.bounded_singleton, not_bounded_iff, bounded_ge_Ioo, bounded_ge_inter_ge, bounded_gt_inter_gt, bounded_gt_Icc, bounded_le_Iio, bounded_lt_Ioo, bounded_ge_Icc, bounded_lt_inter_lt, not_unbounded_iff, bounded_gt_Ico, bounded_ge_Ico, bounded_le_Icc, bounded_le_Iic, bounded_ge_Ici, bounded_ge_iff_bounded_gt, bounded_le_Ioo, bounded_lt_Ico, bounded_le_inter_lt, bounded_gt_Ici, bounded_lt_Ioc, bounded_le_inter_le, bounded_ge_inter_gt, bounded_gt_Ioc, bounded_le_iff_bounded_lt, bounded_inter_not, bounded_le_Ico, bounded_lt_inter_le, bounded_gt_inter_not_gt, bounded_lt_Iic, bounded_lt_Icc, bounded_self, bounded_ge_Ioi

TotallyBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded 📖	mathematical	TotallyBounded PseudoMetricSpace.toUniformSpace	Bornology.IsBounded PseudoMetricSpace.toBornology	—	Metric.totallyBounded_iff zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Bornology.IsBounded.subset Bornology.isBounded_biUnion Metric.isBounded_ball

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_dist_left_atTop_eq_cocompact 📖	mathematical	—	Filter.comap Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Metric.comap_dist_left_atTop Metric.cobounded_eq_cocompact
tendsto_cocompact_of_tendsto_dist_comp_atTop 📖	mathematical	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Filter.atTop Real.instPreorder	Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Filter.Tendsto.mono_right Metric.tendsto_dist_right_atTop_iff Metric.cobounded_le_cocompact
tendsto_dist_left_cocompact_atTop 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Filter.atTop Real.instPreorder	—	Filter.Tendsto.mono_left Metric.tendsto_dist_left_cobounded_atTop Eq.ge Metric.cobounded_eq_cocompact
tendsto_dist_right_cocompact_atTop 📖	mathematical	—	Filter.Tendsto Real Dist.dist PseudoMetricSpace.toDist Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Filter.atTop Real.instPreorder	—	Filter.Tendsto.mono_left Metric.tendsto_dist_right_cobounded_atTop Eq.ge Metric.cobounded_eq_cocompact
totallyBounded_Icc 📖	mathematical	—	TotallyBounded Set.Icc	—	IsCompact.totallyBounded CompactIccSpace.isCompact_Icc
totallyBounded_Ico 📖	mathematical	—	TotallyBounded Set.Ico	—	TotallyBounded.subset Set.Ico_subset_Icc_self totallyBounded_Icc
totallyBounded_Ioc 📖	mathematical	—	TotallyBounded Set.Ioc	—	TotallyBounded.subset Set.Ioc_subset_Icc_self totallyBounded_Icc
totallyBounded_Ioo 📖	mathematical	—	TotallyBounded Set.Ioo	—	TotallyBounded.subset Set.Ioo_subset_Icc_self totallyBounded_Icc

---

← Back to Index