IsBounded

📁 Source: Mathlib/Order/Filter/IsBounded.lean

Statistics

Metric	Count
Definitions IsBounded, IsBounded, tacticIsBoundedDefault, IsBounded, IsBounded	5
Theorems frequently_ge_map_of_frequently_le, frequently_le_map_of_frequently_ge, isBoundedUnder_ge_comp, isBoundedUnder_ge_comp_iff, isBoundedUnder_le_comp, isBoundedUnder_le_comp_iff, isCoboundedUnder_ge_of_isCobounded, isCoboundedUnder_le_of_isCobounded, isBoundedUnder, isBoundedUnder_of_range, isBoundedUnder, isBoundedUnder_of_range, isBoundedUnder, isCobounded_flip, isCobounded_ge, isCobounded_le, mono, bddAbove_range, bddAbove_range_of_cofinite, bddBelow_range, bddBelow_range_of_cofinite, comp, eventually_ge, eventually_le, ge_of_finite, inf, isCoboundedUnder_flip, isCoboundedUnder_ge, isCoboundedUnder_le, le_of_finite, mono, mono_ge, mono_le, sup, frequently_ge, frequently_le, mk, mono, of_frequently_ge, of_frequently_le, frequently_ge, frequently_le, of_frequently_ge, of_frequently_le, isBoundedUnder_comp, isBoundedUnder_ge_atTop, isBoundedUnder_le_atBot, bddAbove_range_of_tendsto_atTop_atBot, bddBelow_range_of_tendsto_atTop_atTop, isBoundedUnder_const, isBoundedUnder_ge_add, isBoundedUnder_ge_inf, isBoundedUnder_ge_inv, isBoundedUnder_ge_neg, isBoundedUnder_ge_sum, isBoundedUnder_iff_eventually_bddAbove, isBoundedUnder_iff_eventually_bddBelow, isBoundedUnder_le_abs, isBoundedUnder_le_add, isBoundedUnder_le_inv, isBoundedUnder_le_mul_of_nonneg, isBoundedUnder_le_neg, isBoundedUnder_le_sum, isBoundedUnder_le_sup, isBoundedUnder_map_iff, isBoundedUnder_of, isBoundedUnder_of_eventually_ge, isBoundedUnder_of_eventually_le, isBoundedUnder_sum, isBounded_bot, isBounded_ge_atTop, isBounded_ge_of_bot, isBounded_iff, isBounded_le_atBot, isBounded_le_of_top, isBounded_principal, isBounded_sup, isBounded_top, isCoboundedUnder_ge_add, isCoboundedUnder_ge_mul_of_nonneg, isCoboundedUnder_ge_of_eventually_le, isCoboundedUnder_ge_of_le, isCoboundedUnder_le_add, isCoboundedUnder_le_of_eventually_le, isCoboundedUnder_le_of_le, isCobounded_bot, isCobounded_ge_of_top, isCobounded_le_of_bot, isCobounded_principal, isCobounded_top, not_isBoundedUnder_of_tendsto_atBot, not_isBoundedUnder_of_tendsto_atTop, frequently_ge_map_of_frequently_ge, frequently_le_map_of_frequently_le, isBoundedUnder_ge_comp, isBoundedUnder_ge_comp_iff, isBoundedUnder_le_comp, isBoundedUnder_le_comp_iff, isCoboundedUnder_ge_of_isCobounded, isCoboundedUnder_le_of_isCobounded, isBoundedUnder_ge_comp, isBoundedUnder_le_comp, isBoundedUnder_ge_finset_inf, isBoundedUnder_ge_finset_inf', isBoundedUnder_le_finset_sup, isBoundedUnder_le_finset_sup', isCoboundedUnder_ge_finset_inf', isCoboundedUnder_le_finset_sup', isCoboundedUnder_le_max	109
Total	114

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frequently_ge_map_of_frequently_le 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Frequently Preorder.toLE	Filter.map	—	Monotone.frequently_le_map_of_frequently_le
frequently_le_map_of_frequently_ge 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Frequently Preorder.toLE	Filter.map	—	Monotone.frequently_ge_map_of_frequently_ge
isBoundedUnder_ge_comp 📖	—	Antitone Filter.IsBoundedUnder Preorder.toLE	—	—	Filter.IsBoundedUnder.comp
isBoundedUnder_ge_comp_iff 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atTop Filter.atBot	Filter.IsBoundedUnder Preorder.toLE	—	Monotone.isBoundedUnder_le_comp_iff OrderDual.noMaxOrder dual_right
isBoundedUnder_le_comp 📖	—	Antitone Filter.IsBoundedUnder Preorder.toLE	—	—	Filter.IsBoundedUnder.comp
isBoundedUnder_le_comp_iff 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atBot Filter.atTop	Filter.IsBoundedUnder Preorder.toLE	—	Monotone.isBoundedUnder_ge_comp_iff OrderDual.noMinOrder dual_right
isCoboundedUnder_ge_of_isCobounded 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.IsCobounded Preorder.toLE	Filter.IsCoboundedUnder	—	Monotone.isCoboundedUnder_le_of_isCobounded
isCoboundedUnder_le_of_isCobounded 📖	mathematical	Antitone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.IsCobounded Preorder.toLE	Filter.IsCoboundedUnder	—	Monotone.isCoboundedUnder_le_of_isCobounded dual

BddAbove

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder 📖	mathematical	Set Filter Filter.instMembership BddAbove Preorder.toLE Set.image	Filter.IsBoundedUnder	—	Filter.isBoundedUnder_iff_eventually_bddAbove
isBoundedUnder_of_range 📖	mathematical	BddAbove Preorder.toLE Set.range	Filter.IsBoundedUnder	—	isBoundedUnder Filter.univ_mem Set.image_univ

BddBelow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder 📖	mathematical	Set Filter Filter.instMembership BddBelow Preorder.toLE Set.image	Filter.IsBoundedUnder	—	Filter.isBoundedUnder_iff_eventually_bddBelow
isBoundedUnder_of_range 📖	mathematical	BddBelow Preorder.toLE Set.range	Filter.IsBoundedUnder	—	isBoundedUnder Filter.univ_mem Set.image_univ

Bornology

Definitions

Name	Category	Theorems
IsBounded 📖	MathDef	116 math math: OrderDual.isBounded_preimage_toDual, ext_iff_isBounded, Metric.isBounded_ball, NormedSpace.isBounded_polar_of_mem_nhds_zero, MonoidHom.exists_nhds_isBounded, Metric.isCompact_iff_isClosed_bounded, Metric.isBounded_closedBall, Metric.isBounded_iff_subset_ball, IsBounded.all, Metric.isBounded_range_of_tendsto_cofinite, isBounded_iff_forall_norm_le', isBounded_biUnion, not_bounded_iff_exists_ne_zero_mem_asymptoticCone, NormedSpace.isBounded_iff_subset_smul_ball, NormedSpace.isVonNBounded_iff, BoxIntegral.Box.isBounded, Metric.isBounded_range_of_tendsto, MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le, orderBornology_isBounded, isBounded_iff_forall_mem, isBounded_iUnion, Metric.isBounded_of_bddAbove_of_bddBelow, BddBelow.isBounded_inter, IsCompact.isBounded, TotallyBounded.isBounded, NormedSpace.isBounded_iff_subset_smul_closedBall, OrderDual.isBounded_preimage_ofDual, Metric.ediam_eq_top_iff_unbounded, isBounded_empty, isBounded_induced, Metric.isBounded_iff_eventually, Metric.isBounded_Ioo, BoundedContinuousFunction.isBounded_range, Metric.Snowflaking.isBounded_preimage_ofSnowflaking_iff, IsCobounded.of_compl, Metric.isBounded_iff_ediam_ne_top, isBounded_insert, Metric.Snowflaking.isBounded_image_ofSnowflaking_iff, BddAbove.isBounded_inter, isBounded_pi_of_nonempty, sUnion_bounded_univ, boundedSpace_subtype_iff, isBounded_iff_asymptoticCone_subset_singleton, BoundedSpace.bounded_univ, isBounded_def, isBounded_image_subtype_val, isBounded_biUnion_finset, isBounded_union, Metric.isBounded_iff, Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn, relativelyCompact.isBounded_iff, BddBelow.isBounded, Metric.exists_isBounded_image_of_tendsto, ZeroAtInftyContinuousMap.isBounded_image, isBounded_iff_of_bilipschitz, bounded_stdSimplex, forall_isBounded_image_eval_iff, ConvexBody.isBounded, spectrum.isBounded, isBounded_convexHull, BoxIntegral.Box.isBounded_Icc, Subalgebra.spectrum_isBounded_connectedComponentIn, isBounded_iff_isVonNBounded, isBounded_image_fst_and_snd, isBounded_iff_forall_norm_le, Set.Finite.isBounded, boundedSpace_val_set_iff, Metric.isBounded_of_compactSpace, Metric.isBounded_image_iff, isBounded_compl_iff, NormedSpace.unbounded_univ, isBounded_univ, isBounded_prod, isBounded_sUnion, isBounded_pi, Metric.isBounded_Ico, Metric.isBounded_closure_iff, IsCobounded.compl, isBounded_prod_self, CauchySeq.isBounded_range, Metric.isBounded_range_of_cauchy_map_cofinite, Metric.isBounded_sphere, Metric.isBounded_iff_nndist, BoundedContinuousFunction.isBounded_range_integral, ZSpan.fundamentalDomain_isBounded, Metric.compactSpace_iff_isBounded_univ, Metric.isBounded_range_of_tendsto_cofinite_uniformity, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, isCobounded_compl_iff, isBounded_iff_bddBelow_bddAbove, Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt, NumberField.mixedEmbedding.fundamentalCone.isBounded_normLeOne, NumberField.mixedEmbedding.convexBodySum_isBounded, Function.Periodic.isBounded_of_continuous, Metric.isBounded_Ioc, ZeroAtInftyContinuousMap.isBounded_range, AddMonoidHom.exists_nhds_isBounded, Metric.Snowflaking.isBounded_preimage_toSnowflaking_iff, Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn, Metric.isBounded_of_abs_le, isBounded_prod_of_nonempty, Metric.isBounded_iff_exists_ge, Filter.HasBasis.disjoint_cobounded_iff, Metric.isBounded_iff_subset_closedBall, Metric.isBounded_Icc, inCompact.isBounded_iff, Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt, comap_cobounded_le_iff, isBounded_ofBounded_iff, boundedSpace_induced_iff, Metric.isBounded_of_abs_lt, isBounded_singleton, BoundedContinuousFunction.isBounded_image, Metric.isBounded_range_iff, BddAbove.isBounded, Metric.Snowflaking.isBounded_image_toSnowflaking_iff

Filter

Definitions

Name	Category	Theorems
IsBounded 📖	MathDef	12 math math: isBounded_iff, isBounded_bot, isBounded_le_atBot, isBounded_le_of_top, BoundedLENhdsClass.isBounded_le_nhds, isBounded_ge_nhds, isBounded_principal, BoundedGENhdsClass.isBounded_ge_nhds, isBounded_ge_atTop, isBounded_ge_of_bot, isBounded_top, isBounded_le_nhds
tacticIsBoundedDefault 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_range_of_tendsto_atTop_atBot 📖	mathematical	Tendsto atTop Nat.instPreorder atBot	BddAbove Preorder.toLE Set.range	—	IsBoundedUnder.bddAbove_range Tendsto.isBoundedUnder_le_atBot
bddBelow_range_of_tendsto_atTop_atTop 📖	mathematical	Tendsto atTop Nat.instPreorder	BddBelow Preorder.toLE Set.range	—	IsBoundedUnder.bddBelow_range Tendsto.isBoundedUnder_ge_atTop
isBoundedUnder_const 📖	mathematical	—	IsBoundedUnder	—	eventually_map Eventually.of_forall refl
isBoundedUnder_ge_add 📖	mathematical	IsBoundedUnder Preorder.toLE	Pi.instAdd	—	mp_mem univ_mem' add_le_add
isBoundedUnder_ge_inf 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder SemilatticeInf.toMin	—	isBoundedUnder_le_sup
isBoundedUnder_ge_inv 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	OrderIso.isBoundedUnder_le_comp IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
isBoundedUnder_ge_neg 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	OrderIso.isBoundedUnder_le_comp IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
isBoundedUnder_ge_sum 📖	mathematical	IsBoundedUnder Preorder.toLE	Finset.sum Pi.addCommMonoid	—	isBoundedUnder_sum isBoundedUnder_ge_add le_rfl
isBoundedUnder_iff_eventually_bddAbove 📖	mathematical	—	IsBoundedUnder Preorder.toLE BddAbove Set.image Eventually Set Set.instMembership	—	Eventually.mono
isBoundedUnder_iff_eventually_bddBelow 📖	mathematical	—	IsBoundedUnder Preorder.toLE BddBelow Set.image Eventually Set Set.instMembership	—	isBoundedUnder_iff_eventually_bddAbove
isBoundedUnder_le_abs 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder abs AddCommGroup.toAddGroup	—	isBoundedUnder_le_sup isBoundedUnder_le_neg
isBoundedUnder_le_add 📖	mathematical	IsBoundedUnder Preorder.toLE	Pi.instAdd	—	mp_mem univ_mem' add_le_add
isBoundedUnder_le_inv 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	OrderIso.isBoundedUnder_ge_comp IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
isBoundedUnder_le_mul_of_nonneg 📖	mathematical	Frequently Preorder.toLE IsBoundedUnder EventuallyLE Pi.instZero	Pi.instMul	—	IsBoundedUnder.eventually_le isBoundedUnder_of_eventually_le mp_mem univ_mem' Frequently.exists Frequently.and_eventually LE.le.trans mul_le_mul_of_nonneg_right mul_le_mul_of_nonneg_left
isBoundedUnder_le_neg 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	OrderIso.isBoundedUnder_ge_comp IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
isBoundedUnder_le_sum 📖	mathematical	IsBoundedUnder Preorder.toLE	Finset.sum Pi.addCommMonoid	—	isBoundedUnder_sum isBoundedUnder_le_add le_rfl
isBoundedUnder_le_sup 📖	mathematical	—	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder SemilatticeSup.toMax	—	IsBoundedUnder.mono_le Eventually.of_forall le_sup_left le_sup_right IsBoundedUnder.sup
isBoundedUnder_map_iff 📖	mathematical	—	IsBoundedUnder map	—	—
isBoundedUnder_of 📖	mathematical	—	IsBoundedUnder	—	Eventually.of_forall
isBoundedUnder_of_eventually_ge 📖	mathematical	Eventually Preorder.toLE	IsBoundedUnder	—	—
isBoundedUnder_of_eventually_le 📖	mathematical	Eventually Preorder.toLE	IsBoundedUnder	—	—
isBoundedUnder_sum 📖	mathematical	IsBoundedUnder Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	Finset.sum Pi.addCommMonoid	—	Finset.cons_induction Finset.sum_empty Finset.sum_cons
isBounded_bot 📖	mathematical	—	IsBounded Bot.bot Filter instBot	—	—
isBounded_ge_atTop 📖	mathematical	—	IsBounded Preorder.toLE atTop	—	eventually_ge_atTop
isBounded_ge_of_bot 📖	mathematical	—	IsBounded	—	Eventually.of_forall bot_le
isBounded_iff 📖	mathematical	—	IsBounded Set Set.instMembership sets Set.instHasSubset setOf	—	Set.Subset.refl mem_of_superset
isBounded_le_atBot 📖	mathematical	—	IsBounded Preorder.toLE atBot	—	eventually_le_atBot
isBounded_le_of_top 📖	mathematical	—	IsBounded	—	Eventually.of_forall le_top
isBounded_principal 📖	mathematical	—	IsBounded principal	—	—
isBounded_sup 📖	mathematical	IsBounded	Filter instSup	—	directed_of eventually_sup Eventually.mono trans
isBounded_top 📖	mathematical	—	IsBounded Top.top Filter instTop	—	—
isCoboundedUnder_ge_add 📖	mathematical	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsCoboundedUnder	Pi.instAdd	—	IsBoundedUnder.eventually_le IsCoboundedUnder.frequently_le IsCoboundedUnder.of_frequently_le Frequently.mono Frequently.and_eventually add_le_add
isCoboundedUnder_ge_mul_of_nonneg 📖	mathematical	EventuallyLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Pi.instZero IsBoundedUnder IsCoboundedUnder	Pi.instMul	—	IsBoundedUnder.eventually_le IsCoboundedUnder.frequently_le IsCoboundedUnder.of_frequently_le Frequently.mono Frequently.and_eventually Eventually.and LE.le.trans mul_le_mul_of_nonneg_right mul_le_mul_of_nonneg_left
isCoboundedUnder_ge_of_eventually_le 📖	mathematical	Eventually Preorder.toLE	IsCoboundedUnder	—	IsBoundedUnder.isCoboundedUnder_ge
isCoboundedUnder_ge_of_le 📖	mathematical	Preorder.toLE	IsCoboundedUnder	—	isCoboundedUnder_ge_of_eventually_le Eventually.of_forall
isCoboundedUnder_le_add 📖	mathematical	IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsCoboundedUnder	Pi.instAdd	—	IsBoundedUnder.eventually_ge IsCoboundedUnder.frequently_ge IsCoboundedUnder.of_frequently_ge Frequently.mono Frequently.and_eventually add_le_add
isCoboundedUnder_le_of_eventually_le 📖	mathematical	Eventually Preorder.toLE	IsCoboundedUnder	—	IsBoundedUnder.isCoboundedUnder_le
isCoboundedUnder_le_of_le 📖	mathematical	Preorder.toLE	IsCoboundedUnder	—	isCoboundedUnder_le_of_eventually_le Eventually.of_forall
isCobounded_bot 📖	mathematical	—	IsCobounded Bot.bot Filter instBot	—	—
isCobounded_ge_of_top 📖	mathematical	—	IsCobounded	—	le_top
isCobounded_le_of_bot 📖	mathematical	—	IsCobounded	—	bot_le
isCobounded_principal 📖	mathematical	—	IsCobounded principal	—	—
isCobounded_top 📖	mathematical	—	IsCobounded Top.top Filter instTop	—	—
not_isBoundedUnder_of_tendsto_atBot 📖	mathematical	Tendsto atBot	IsBoundedUnder Preorder.toLE	—	not_isBoundedUnder_of_tendsto_atTop OrderDual.noMaxOrder
not_isBoundedUnder_of_tendsto_atTop 📖	mathematical	Tendsto atTop	IsBoundedUnder Preorder.toLE	—	NoMaxOrder.exists_gt tendsto_atTop Set.eq_empty_of_subset_empty not_le_of_gt le_trans Set.Nonempty.ne_empty nonempty_of_mem Eventually.and eventually_map

Filter.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder 📖	mathematical	Filter.IsBounded	Filter.IsBoundedUnder	—	Filter.Eventually.mono
isCobounded_flip 📖	mathematical	Filter.IsBounded	Filter.IsCobounded	—	Filter.Eventually.exists Filter.Eventually.and trans
isCobounded_ge 📖	mathematical	Filter.IsBounded Preorder.toLE	Filter.IsCobounded	—	isCobounded_flip instIsTransLe
isCobounded_le 📖	mathematical	Filter.IsBounded Preorder.toLE	Filter.IsCobounded	—	isCobounded_flip instIsTransGe
mono 📖	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.IsBounded	—	—	—

Filter.IsBoundedUnder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_range 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE Filter.atTop Nat.instPreorder	BddAbove Set.range	—	bddAbove_range_of_cofinite Nat.cofinite_eq_atTop
bddAbove_range_of_cofinite 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE Filter.cofinite	BddAbove Set.range	—	Set.image_univ Set.union_compl_self Set.image_union bddAbove_union Set.forall_mem_image Set.Finite.bddAbove Set.Finite.image
bddBelow_range 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE Filter.atTop Nat.instPreorder	BddBelow Set.range	—	bddAbove_range OrderDual.isDirected_le
bddBelow_range_of_cofinite 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE Filter.cofinite	BddBelow Set.range	—	bddAbove_range_of_cofinite OrderDual.isDirected_le
comp 📖	—	Filter.IsBoundedUnder	—	—	Filter.Eventually.mono
eventually_ge 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE	Filter.Eventually	—	eventually_le
eventually_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE	Filter.Eventually	—	—
ge_of_finite 📖	mathematical	—	Filter.IsBoundedUnder Preorder.toLE	—	BddBelow.isBoundedUnder_of_range Set.Finite.bddBelow Set.toFinite Finite.Set.finite_range
inf 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder	SemilatticeInf.toMin	—	sup
isCoboundedUnder_flip 📖	mathematical	Filter.IsBoundedUnder	Filter.IsCoboundedUnder	—	Filter.IsBounded.isCobounded_flip Filter.map_neBot
isCoboundedUnder_ge 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE	Filter.IsCoboundedUnder	—	isCoboundedUnder_flip instIsTransLe
isCoboundedUnder_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE	Filter.IsCoboundedUnder	—	isCoboundedUnder_flip instIsTransGe
le_of_finite 📖	mathematical	—	Filter.IsBoundedUnder Preorder.toLE	—	BddAbove.isBoundedUnder_of_range Set.Finite.bddAbove Set.toFinite Finite.Set.finite_range
mono 📖	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.IsBoundedUnder	—	—	Filter.IsBounded.mono Filter.map_mono
mono_ge 📖	—	Filter.IsBoundedUnder Preorder.toLE Filter.EventuallyLE	—	—	mono_le
mono_le 📖	—	Filter.IsBoundedUnder Preorder.toLE Filter.EventuallyLE	—	—	Filter.Eventually.mp Filter.eventually_map Filter.Eventually.mono le_trans
sup 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	SemilatticeSup.toMax	—	Filter.mp_mem Filter.univ_mem' sup_le_sup

Filter.IsCobounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frequently_ge 📖	mathematical	Filter.IsCobounded Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Frequently	—	isBot_or_exists_lt SemilatticeInf.instIsCodirectedOrder Filter.Frequently.of_forall not_lt_of_ge Filter.mp_mem Filter.univ_mem' LT.lt.le not_le
frequently_le 📖	mathematical	Filter.IsCobounded Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Frequently	—	frequently_ge
mk 📖	mathematical	Set Set.instMembership	Filter.IsCobounded	—	trans
mono 📖	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.IsCobounded	—	—	—
of_frequently_ge 📖	mathematical	Filter.Frequently Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.IsCobounded	—	isBot_or_exists_lt SemilatticeInf.instIsCodirectedOrder Filter.Frequently.exists Filter.Frequently.and_eventually LE.le.trans LT.lt.le
of_frequently_le 📖	mathematical	Filter.Frequently Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.IsCobounded	—	of_frequently_ge

Filter.IsCoboundedUnder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frequently_ge 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Frequently	—	Filter.IsCobounded.frequently_ge Filter.map_neBot
frequently_le 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Frequently	—	Filter.IsCobounded.frequently_le Filter.map_neBot
of_frequently_ge 📖	mathematical	Filter.Frequently Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.IsCoboundedUnder	—	Filter.IsCobounded.of_frequently_ge
of_frequently_le 📖	mathematical	Filter.Frequently Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.IsCoboundedUnder	—	Filter.IsCobounded.of_frequently_le

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder_comp 📖	—	Filter.Tendsto Filter.IsBoundedUnder	—	—	Filter.isBoundedUnder_map_iff Filter.IsBoundedUnder.mono
isBoundedUnder_ge_atTop 📖	mathematical	Filter.Tendsto Filter.atTop	Filter.IsBoundedUnder Preorder.toLE	—	Filter.IsBounded.mono Filter.isBounded_ge_atTop
isBoundedUnder_le_atBot 📖	mathematical	Filter.Tendsto Filter.atBot	Filter.IsBoundedUnder Preorder.toLE	—	Filter.IsBounded.mono Filter.isBounded_le_atBot

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frequently_ge_map_of_frequently_ge 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Frequently Preorder.toLE	Filter.map	—	Filter.mp_mem Filter.univ_mem' lt_irrefl lt_of_le_of_lt not_lt
frequently_le_map_of_frequently_le 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Frequently Preorder.toLE	Filter.map	—	Filter.mp_mem Filter.univ_mem' lt_irrefl lt_of_lt_of_le not_lt
isBoundedUnder_ge_comp 📖	—	Monotone Filter.IsBoundedUnder Preorder.toLE	—	—	Filter.IsBoundedUnder.comp
isBoundedUnder_ge_comp_iff 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atBot	Filter.IsBoundedUnder Preorder.toLE	—	isBoundedUnder_le_comp_iff OrderDual.instNonempty OrderDual.noMaxOrder dual
isBoundedUnder_le_comp 📖	—	Monotone Filter.IsBoundedUnder Preorder.toLE	—	—	Filter.IsBoundedUnder.comp
isBoundedUnder_le_comp_iff 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto Filter.atTop	Filter.IsBoundedUnder Preorder.toLE	—	Filter.eventually_atTop SemilatticeSup.instIsDirectedOrder Filter.Tendsto.eventually_gt_atTop instNoTopOrderOfNoMaxOrder Filter.Eventually.mono Filter.eventually_map not_lt LT.lt.not_ge LT.lt.le Filter.IsBounded.isBoundedUnder
isCoboundedUnder_ge_of_isCobounded 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.IsCobounded Preorder.toLE	Filter.IsCoboundedUnder	—	isCoboundedUnder_le_of_isCobounded dual
isCoboundedUnder_le_of_isCobounded 📖	mathematical	Monotone PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.IsCobounded Preorder.toLE	Filter.IsCoboundedUnder	—	Filter.IsCobounded.frequently_ge Filter.IsCobounded.of_frequently_ge frequently_ge_map_of_frequently_ge

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder_ge_comp 📖	mathematical	—	Filter.IsBoundedUnder DFunLike.coe OrderIso instFunLikeOrderIso	—	isBoundedUnder_le_comp
isBoundedUnder_le_comp 📖	mathematical	—	Filter.IsBoundedUnder DFunLike.coe OrderIso instFunLikeOrderIso	—	Function.Surjective.exists surjective le_iff_le

RingHom

Definitions

Name	Category	Theorems
IsBounded 📖	MathDef	—

Seminorm

Definitions

Name	Category	Theorems
IsBounded 📖	MathDef	2 math math: isBounded_const, const_isBounded

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder_ge_finset_inf 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.inf	—	isBoundedUnder_le_finset_sup
isBoundedUnder_ge_finset_inf' 📖	mathematical	Finset.Nonempty Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.inf'	—	isBoundedUnder_le_finset_sup' OrderDual.instNonempty
isBoundedUnder_le_finset_sup 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.sup Lattice.toSemilatticeSup	—	Filter.Eventually.mono Filter.eventually_all_finset Finset.sup_mono_fun bot_nonempty Function.sometimes_spec
isBoundedUnder_le_finset_sup' 📖	mathematical	Finset.Nonempty Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.sup' Lattice.toSemilatticeSup	—	Filter.Eventually.mono Filter.eventually_all_finset le_trans Finset.le_sup' Function.sometimes_spec
isCoboundedUnder_ge_finset_inf' 📖	mathematical	Finset.Nonempty Finset Finset.instMembership Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.inf'	—	isCoboundedUnder_le_finset_sup'
isCoboundedUnder_le_finset_sup' 📖	mathematical	Finset.Nonempty Finset Finset.instMembership Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Finset.sup' Lattice.toSemilatticeSup	—	Filter.eventually_map Filter.Eventually.mono
isCoboundedUnder_le_max 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	SemilatticeSup.toMax Lattice.toSemilatticeSup	—	Filter.eventually_map Filter.Eventually.mono

---

← Back to Index