Bounded

📁 Source: Mathlib/Analysis/Normed/Group/Bounded.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_norm_le, exists_norm_le', exists_pos_norm_le, exists_pos_norm_le', exists_pos_norm_lt, exists_pos_norm_lt', bounded_above_of_compact_support, cobounded_of_norm, cobounded_of_norm', op_one_isBoundedUnder_le, op_one_isBoundedUnder_le', op_zero_isBoundedUnder_le, op_zero_isBoundedUnder_le', hasBasis_cobounded_norm, hasBasis_cobounded_norm', inv_cobounded, neg_cobounded, tendsto_inv_cobounded, tendsto_neg_cobounded, exists_bound_of_continuous, exists_pos_le_norm, exists_bound_of_continuous, exists_pos_le_norm, exists_bound_of_continuousOn, exists_bound_of_continuousOn', cauchySeq_iff, cauchySeq_iff, comap_norm_atTop, comap_norm_atTop', eventually_cobounded_le_norm, eventually_cobounded_le_norm', isBounded_iff_forall_norm_le, isBounded_iff_forall_norm_le', tendsto_norm_atTop_iff_cobounded, tendsto_norm_atTop_iff_cobounded', tendsto_norm_cobounded_atTop, tendsto_norm_cobounded_atTop', tendsto_norm_cocompact_atTop, tendsto_norm_cocompact_atTop', tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding'	41
Total	41

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_norm_le 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	isBounded_iff_forall_norm_le
exists_norm_le' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	isBounded_iff_forall_norm_le'
exists_pos_norm_le 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	exists_norm_le lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LE.le.trans le_max_left
exists_pos_norm_le' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	Real Real.instLT Real.instZero Real.instLE Norm.norm SeminormedGroup.toNorm	—	exists_norm_le' lt_max_of_lt_right Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LE.le.trans le_max_left
exists_pos_norm_lt 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLT Real.instZero Norm.norm SeminormedAddGroup.toNorm	—	exists_pos_norm_le add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LE.le.trans_lt lt_add_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd
exists_pos_norm_lt' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	Real Real.instLT Real.instZero Norm.norm SeminormedGroup.toNorm	—	exists_pos_norm_le' add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one LE.le.trans_lt lt_add_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounded_above_of_compact_support 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NormedAddGroup.toSeminormedAddGroup HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid NormedAddGroup.toAddGroup	Real Real.instLE Norm.norm NormedAddGroup.toNorm	—	bddAbove_range_of_hasCompactSupport instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal norm HasCompactSupport.norm

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasBasis_cobounded_norm 📖	mathematical	—	HasBasis Real Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace setOf Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	HasBasis.cobounded_of_norm atTop_basis instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
hasBasis_cobounded_norm' 📖	mathematical	—	HasBasis Real Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace setOf Real.instLE Norm.norm SeminormedGroup.toNorm	—	HasBasis.cobounded_of_norm' atTop_basis instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean
inv_cobounded 📖	mathematical	—	Filter instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	—	comap_comap norm_inv'
neg_cobounded 📖	mathematical	—	Filter instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	—	comap_norm_atTop comap_neg comap_comap norm_neg
tendsto_inv_cobounded 📖	mathematical	—	Tendsto InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	—	Eq.le inv_cobounded
tendsto_neg_cobounded 📖	mathematical	—	Tendsto NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	—	Eq.le neg_cobounded

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cobounded_of_norm 📖	mathematical	Filter.HasBasis Real Filter.atTop Real.instPreorder	Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace Set.preimage Norm.norm SeminormedAddGroup.toNorm	—	comap comap_norm_atTop
cobounded_of_norm' 📖	mathematical	Filter.HasBasis Real Filter.atTop Real.instPreorder	Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace Set.preimage Norm.norm SeminormedGroup.toNorm	—	comap comap_norm_atTop'

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_one_isBoundedUnder_le 📖	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Filter.IsBoundedUnder Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instMul	—	—	op_one_isBoundedUnder_le' one_mul
op_one_isBoundedUnder_le' 📖	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Filter.IsBoundedUnder Real Real.instLE Norm.norm SeminormedGroup.toNorm Real.instMul	—	—	NormedCommGroup.tendsto_nhds_one exists_pos_mul_lt Real.instIsStrictOrderedRing Filter.mp_mem Filter.eventually_map Filter.univ_mem' LE.le.trans_lt le_total mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg' mul_le_mul IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_left le_of_lt mul_nonneg mul_right_comm
op_zero_isBoundedUnder_le 📖	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Filter.IsBoundedUnder Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instMul	—	—	op_zero_isBoundedUnder_le' one_mul
op_zero_isBoundedUnder_le' 📖	—	Filter.Tendsto nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Filter.IsBoundedUnder Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Real.instMul	—	—	NormedAddCommGroup.tendsto_nhds_zero exists_pos_mul_lt Real.instIsStrictOrderedRing Filter.mp_mem Filter.eventually_map Filter.univ_mem' LE.le.trans_lt le_total mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg mul_le_mul IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_left le_of_lt mul_nonneg mul_right_comm

HasCompactMulSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bound_of_continuous 📖	mathematical	HasCompactMulSupport InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid SeminormedGroup.toGroup Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	Bornology.IsBounded.exists_norm_le' IsCompact.isBounded isCompact_range
exists_pos_le_norm 📖	mathematical	HasCompactMulSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NormedAddGroup.toSeminormedAddGroup	Real Real.instLT Real.instZero	—	exists_compact_iff_hasCompactMulSupport instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace Bornology.IsBounded.exists_pos_norm_le IsCompact.isBounded add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Contrapose.contrapose₃ lt_add_of_le_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bound_of_continuous 📖	mathematical	HasCompactSupport NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid SeminormedAddGroup.toAddGroup Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	Set.mem_range Bornology.IsBounded.exists_norm_le IsCompact.isBounded isCompact_range
exists_pos_le_norm 📖	mathematical	HasCompactSupport UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace NormedAddGroup.toSeminormedAddGroup	Real Real.instLT Real.instZero	—	exists_compact_iff_hasCompactSupport instR1Space TopologicalSpace.PseudoMetrizableSpace.regularSpace PseudoEMetricSpace.pseudoMetrizableSpace Bornology.IsBounded.exists_pos_norm_le IsCompact.isBounded add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Contrapose.contrapose₃ not_le lt_add_of_le_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_bound_of_continuousOn 📖	mathematical	IsCompact ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	Set.mem_image_of_mem isBounded_iff_forall_norm_le isBounded image_of_continuousOn
exists_bound_of_continuousOn' 📖	mathematical	IsCompact ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	Set.mem_image_of_mem isBounded_iff_forall_norm_le' isBounded image_of_continuousOn

NormedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_iff 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder Real Real.instLT Norm.norm SeminormedAddGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	Metric.cauchySeq_iff dist_eq_norm_sub

NormedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_iff 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder Real Real.instLT Norm.norm SeminormedGroup.toNorm DivInvMonoid.toDiv Group.toDivInvMonoid SeminormedGroup.toGroup	—	dist_eq_norm_div

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_norm_atTop 📖	mathematical	—	Filter.comap Real Norm.norm SeminormedAddGroup.toNorm Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	—	dist_zero_right Metric.comap_dist_right_atTop
comap_norm_atTop' 📖	mathematical	—	Filter.comap Real Norm.norm SeminormedGroup.toNorm Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	—	dist_one_right Metric.comap_dist_right_atTop
eventually_cobounded_le_norm 📖	mathematical	—	Filter.Eventually Real Real.instLE Norm.norm SeminormedAddGroup.toNorm Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	—	Filter.Tendsto.eventually_ge_atTop tendsto_norm_cobounded_atTop
eventually_cobounded_le_norm' 📖	mathematical	—	Filter.Eventually Real Real.instLE Norm.norm SeminormedGroup.toNorm Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	—	Filter.Tendsto.eventually_ge_atTop tendsto_norm_cobounded_atTop'
isBounded_iff_forall_norm_le 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedAddGroup.toNorm	—	mem_closedBall_zero_iff Metric.isBounded_iff_subset_closedBall
isBounded_iff_forall_norm_le' 📖	mathematical	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace Real Real.instLE Norm.norm SeminormedGroup.toNorm	—	Metric.isBounded_iff_subset_closedBall
tendsto_norm_atTop_iff_cobounded 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedAddGroup.toNorm Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace	—	comap_norm_atTop Filter.tendsto_comap_iff
tendsto_norm_atTop_iff_cobounded' 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedGroup.toNorm Filter.atTop Real.instPreorder Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace	—	comap_norm_atTop' Filter.tendsto_comap_iff
tendsto_norm_cobounded_atTop 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedAddGroup.toNorm Bornology.cobounded PseudoMetricSpace.toBornology SeminormedAddGroup.toPseudoMetricSpace Filter.atTop Real.instPreorder	—	tendsto_norm_atTop_iff_cobounded Filter.tendsto_id
tendsto_norm_cobounded_atTop' 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedGroup.toNorm Bornology.cobounded PseudoMetricSpace.toBornology SeminormedGroup.toPseudoMetricSpace Filter.atTop Real.instPreorder	—	tendsto_norm_atTop_iff_cobounded' Filter.tendsto_id
tendsto_norm_cocompact_atTop 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedAddGroup.toNorm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace Filter.atTop Real.instPreorder	—	tendsto_norm_cobounded_atTop Metric.cobounded_eq_cocompact
tendsto_norm_cocompact_atTop' 📖	mathematical	—	Filter.Tendsto Real Norm.norm SeminormedGroup.toNorm Filter.cocompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace Filter.atTop Real.instPreorder	—	tendsto_norm_cobounded_atTop' Metric.cobounded_eq_cocompact
tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding 📖	mathematical	Topology.IsClosedEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace	Filter.Tendsto Real Norm.norm SeminormedAddGroup.toNorm Filter.cofinite Filter.atTop Real.instPreorder	—	Filter.cocompact_eq_cofinite Filter.Tendsto.comp tendsto_norm_cocompact_atTop Topology.IsClosedEmbedding.tendsto_cocompact
tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding' 📖	mathematical	Topology.IsClosedEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedGroup.toPseudoMetricSpace	Filter.Tendsto Real Norm.norm SeminormedGroup.toNorm Filter.cofinite Filter.atTop Real.instPreorder	—	Filter.cocompact_eq_cofinite Filter.Tendsto.comp tendsto_norm_cocompact_atTop' Topology.IsClosedEmbedding.tendsto_cocompact

---

← Back to Index