Basic

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

Statistics

Metric	Count
Definitions IsCobounded, cobounded, cobounded', cofinite, ofBounded, ofBounded', BoundedSpace, instBornology, instBornologyPUnit	9
Theorems all, compl, insert, of_compl, subset, union, all, compl, inter, of_compl, superset, cobounded_eq_bot, cobounded_eq_bot_iff, comap_cobounded_le_iff, eventually_ne_cobounded, ext, ext_iff, ext_iff', ext_iff_isBounded, isBounded_biUnion, isBounded_biUnion_finset, isBounded_compl_iff, isBounded_def, isBounded_empty, isBounded_iUnion, isBounded_iff_forall_mem, isBounded_insert, isBounded_ofBounded_iff, isBounded_sUnion, isBounded_singleton, isBounded_union, isBounded_univ, isCobounded_biInter, isCobounded_biInter_finset, isCobounded_compl_iff, isCobounded_def, isCobounded_iInter, isCobounded_inter, isCobounded_ofBounded_iff, isCobounded_sInter, isCobounded_univ, le_cofinite, le_cofinite', nonempty_of_not_isBounded, ofBounded'_cobounded, ofBounded_cobounded, sUnion_bounded_univ, bounded_univ, of_finite, disjoint_cobounded_iff, eventually_ne_cobounded, isBounded_preimage_ofDual, isBounded_preimage_toDual, isCobounded_preimage_ofDual, isCobounded_preimage_toDual, isBounded	56
Total	65

Bornology

Definitions

Name	Category	Theorems
IsCobounded 📖	MathDef	16 math math: isCobounded_iInter, isCobounded_inter, isCobounded_biInter_finset, isCobounded_ofBounded_iff, IsCobounded.all, isBounded_compl_iff, IsBounded.compl, IsBounded.of_compl, Metric.isCobounded_iff_closedBall_compl_subset, isCobounded_compl_iff, isCobounded_univ, OrderDual.isCobounded_preimage_ofDual, isCobounded_sInter, isCobounded_def, OrderDual.isCobounded_preimage_toDual, isCobounded_biInter
cobounded 📖	CompOp	105 math math: Metric.hasBasis_cobounded_compl_closedBall, tendsto_const_sub_cobounded, eventually_ne_cobounded, tendsto_const_add_cobounded, Filter.hasBasis_cobounded_norm', Complex.comap_exp_cobounded, Metric.hasAntitoneBasis_cobounded_compl_ball, tendsto_cobounded_iff_meromorphicOrderAt_neg, Filter.inv_nhdsWithin_ne_zero, AffineSpace.cobounded_eq_iSup_sphere_asymptoticNhds, tendsto_zpow_nhdsNE_zero_cobounded, eventually_cobounded_le_norm, Metric.comap_dist_left_atTop, DilationEquiv.map_cobounded, Filter.map_mul_left_cobounded, comap_norm_atTop', AntilipschitzWith.tendsto_cobounded, Filter.map_mul_right_cobounded, Filter.inv_nhdsNE_zero, RealNormedSpace.cobounded_neBot, Metric.disjoint_cobounded_nhdsSet, ext_iff, Metric.comap_dist_right_atTop, LocallyBoundedMap.comap_cobounded_le', bornology_eq_of_bilipschitz, le_cofinite, tendsto_cobounded_of_meromorphicOrderAt_neg, Complex.tendsto_exp_comap_re_atTop, Metric.disjoint_nhds_cobounded, Filter.inv_cobounded₀, tendsto_sub_const_cobounded, ofBounded'_cobounded, Asymptotics.isLittleO_const_id_cobounded, Complex.map_exp_comap_re_atTop, eventually_cobounded_mapsTo, Filter.tendsto_inv₀_cobounded, tendsto_intCast_atBot_sup_atTop_cobounded, Unitization.cobounded_eq_aux, Metric.cobounded_le_cocompact, spectrum.eventually_isUnit_resolvent, Filter.tendsto_inv_cobounded, Metric.tendsto_dist_left_atTop_iff, Metric.tendsto_dist_left_cobounded_atTop, isBounded_def, Filter.HasBasis.cobounded_of_norm', Filter.hasBasis_cobounded_norm, Absorbs.eventually, Metric.tendsto_dist_right_cobounded_atTop, Metric.hasBasis_cobounded_compl_ball, Metric.hasAntitoneBasis_cobounded_compl_closedBall, ext_iff', RCLike.tendsto_ofReal_cobounded_cobounded, LipschitzWith.comap_cobounded_le, cobounded_eq_bot, absorbs_iff_eventually_cobounded_mapsTo, NontriviallyNormedField.cobounded_neBot, eventually_cobounded_le_norm', Filter.tendsto_inv₀_nhdsWithin_ne_zero, PseudoMetricSpace.cobounded_sets, comap_norm_atTop, le_cofinite', cobounded_eq_bot_iff, Filter.HasBasis.cobounded_of_norm, Dilation.comap_cobounded, Dilation.tendsto_cobounded, Metric.cobounded_eq_cocompact, Metric.disjoint_cobounded_nhds, LocallyBoundedMapClass.comap_cobounded_le, tendsto_norm_atTop_iff_cobounded', AffineSpace.asymptoticNhds_le_cobounded, Filter.neg_cobounded, tendsto_norm_cobounded_atTop', Filter.tendsto_mul_left_cobounded, tendsto_norm_cobounded_atTop, Real.cobounded_eq, Filter.comap_mul_left_cobounded, spectrum.resolvent_tendsto_cobounded, tendsto_norm_atTop_iff_cobounded, absorbent_iff_inv_smul, tendsto_add_const_cobounded, NormedSpace.cobounded_neBot, Filter.comap_mul_right_cobounded, tendsto_intCast_atTop_cobounded, Filter.tendsto_mul_right_cobounded, Filter.tendsto_inv₀_nhdsNE_zero, Filter.HasBasis.disjoint_cobounded_iff, RCLike.tendsto_ofReal_atBot_cobounded, Metric.disjoint_nhdsSet_cobounded, tendsto_pow_cobounded_cobounded, tendsto_algebraMap_cobounded, isCobounded_def, spectrum.resolvent_isBigO_inv, Filter.tendsto_neg_cobounded, ofBounded_cobounded, cobounded_prod, cobounded_pi, tendsto_intCast_atBot_cobounded, algebraMap_cobounded_le_cobounded, comap_cobounded_le_iff, Metric.tendsto_dist_right_atTop_iff, RCLike.tendsto_ofReal_atTop_cobounded, Filter.tendsto_inv₀_cobounded', Int.cobounded_eq, Filter.inv_cobounded, tendsto_natCast_atTop_cobounded
cobounded' 📖	CompOp	—
cofinite 📖	CompOp	—
ofBounded 📖	CompOp	3 math math: isCobounded_ofBounded_iff, ofBounded_cobounded, isBounded_ofBounded_iff
ofBounded' 📖	CompOp	1 math math: ofBounded'_cobounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cobounded_eq_bot 📖	mathematical	—	cobounded Bot.bot Filter Filter.instBot	—	cobounded_eq_bot_iff
cobounded_eq_bot_iff 📖	mathematical	—	cobounded Bot.bot Filter Filter.instBot BoundedSpace	—	isBounded_univ isBounded_def Set.compl_univ Filter.empty_mem_iff_bot
comap_cobounded_le_iff 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap cobounded IsBounded Set.image	—	IsBounded.compl IsBounded.subset IsCobounded.compl HasSubset.Subset.trans Set.instIsTransSubset Set.image_mono Set.preimage_compl Set.subset_compl_comm Set.image_preimage_subset Set.compl_subset_comm Set.subset_preimage_image
eventually_ne_cobounded 📖	mathematical	—	Filter.Eventually cobounded	—	Filter.le_cofinite_iff_eventually_ne le_cofinite
ext 📖	—	cobounded	—	—	—
ext_iff 📖	mathematical	—	cobounded	—	ext
ext_iff' 📖	mathematical	—	Set Filter Filter.instMembership cobounded	—	ext_iff Filter.ext_iff
ext_iff_isBounded 📖	mathematical	—	IsBounded	—	ext_iff' Function.Surjective.forall compl_surjective
isBounded_biUnion 📖	mathematical	—	IsBounded Set.iUnion Set Set.instMembership	—	Set.compl_iUnion isCobounded_biInter
isBounded_biUnion_finset 📖	mathematical	—	IsBounded Set.iUnion Finset Finset.instMembership	—	isBounded_biUnion Finset.finite_toSet
isBounded_compl_iff 📖	mathematical	—	IsBounded Compl.compl Set Set.instCompl IsCobounded	—	isBounded_def isCobounded_def compl_compl
isBounded_def 📖	mathematical	—	IsBounded Set Filter Filter.instMembership cobounded Compl.compl Set.instCompl	—	—
isBounded_empty 📖	mathematical	—	IsBounded Set Set.instEmptyCollection	—	isBounded_def Set.compl_empty Filter.univ_mem
isBounded_iUnion 📖	mathematical	—	IsBounded Set.iUnion	—	Set.sUnion_range isBounded_sUnion Set.finite_range Set.forall_mem_range
isBounded_iff_forall_mem 📖	mathematical	—	IsBounded	—	Set.eq_empty_or_nonempty isBounded_empty
isBounded_insert 📖	mathematical	—	IsBounded Set Set.instInsert	—	IsBounded.subset Set.subset_insert IsBounded.insert
isBounded_ofBounded_iff 📖	mathematical	Set Set.instMembership Set.instEmptyCollection Set.instUnion Set.instSingletonSet	IsBounded ofBounded	—	isBounded_def ofBounded_cobounded
isBounded_sUnion 📖	mathematical	—	IsBounded Set.sUnion	—	Set.sUnion_eq_biUnion isBounded_biUnion
isBounded_singleton 📖	mathematical	—	IsBounded Set Set.instSingletonSet	—	isBounded_def le_cofinite Set.Finite.compl_mem_cofinite Set.finite_singleton
isBounded_union 📖	mathematical	—	IsBounded Set Set.instUnion	—	Set.compl_union
isBounded_univ 📖	mathematical	—	IsBounded Set.univ BoundedSpace	—	BoundedSpace.bounded_univ
isCobounded_biInter 📖	mathematical	—	IsCobounded Set.iInter Set Set.instMembership	—	Filter.biInter_mem
isCobounded_biInter_finset 📖	mathematical	—	IsCobounded Set.iInter Finset Finset.instMembership	—	Filter.biInter_finset_mem
isCobounded_compl_iff 📖	mathematical	—	IsCobounded Compl.compl Set Set.instCompl IsBounded	—	—
isCobounded_def 📖	mathematical	—	IsCobounded Set Filter Filter.instMembership cobounded	—	—
isCobounded_iInter 📖	mathematical	—	IsCobounded Set.iInter	—	Filter.iInter_mem
isCobounded_inter 📖	mathematical	—	IsCobounded Set Set.instInter	—	Filter.inter_mem_iff
isCobounded_ofBounded_iff 📖	mathematical	Set Set.instMembership Set.instEmptyCollection Set.instUnion Set.instSingletonSet	IsCobounded ofBounded Compl.compl Set.instCompl	—	—
isCobounded_sInter 📖	mathematical	—	IsCobounded Set.sInter	—	Filter.sInter_mem
isCobounded_univ 📖	mathematical	—	IsCobounded Set.univ	—	Filter.univ_mem
le_cofinite 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder cobounded Filter.cofinite	—	—
le_cofinite' 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder cobounded Filter.cofinite	—	le_cofinite
nonempty_of_not_isBounded 📖	mathematical	IsBounded	Set.Nonempty	—	Set.nonempty_iff_ne_empty isBounded_empty
ofBounded'_cobounded 📖	mathematical	Set Set.instMembership Set.instEmptyCollection Set.instUnion Set.sUnion Set.univ	cobounded ofBounded'	—	—
ofBounded_cobounded 📖	mathematical	Set Set.instMembership Set.instEmptyCollection Set.instUnion Set.instSingletonSet	cobounded ofBounded	—	—
sUnion_bounded_univ 📖	mathematical	—	Set.sUnion setOf Set IsBounded Set.univ	—	Set.sUnion_eq_univ_iff isBounded_singleton Set.mem_singleton

Bornology.IsBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all 📖	mathematical	—	Bornology.IsBounded	—	subset BoundedSpace.bounded_univ Set.subset_univ
compl 📖	mathematical	Bornology.IsBounded	Bornology.IsCobounded Compl.compl Set Set.instCompl	—	Bornology.isCobounded_compl_iff
insert 📖	mathematical	Bornology.IsBounded	Set Set.instInsert	—	union Bornology.isBounded_singleton
of_compl 📖	mathematical	Bornology.IsBounded Compl.compl Set Set.instCompl	Bornology.IsCobounded	—	Bornology.isBounded_compl_iff
subset 📖	—	Bornology.IsBounded Set Set.instHasSubset	—	—	Bornology.IsCobounded.superset Set.compl_subset_compl
union 📖	mathematical	Bornology.IsBounded	Set Set.instUnion	—	Bornology.isBounded_union

Bornology.IsCobounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
all 📖	mathematical	—	Bornology.IsCobounded	—	Bornology.IsBounded.all compl_compl
compl 📖	mathematical	Bornology.IsCobounded	Bornology.IsBounded Compl.compl Set Set.instCompl	—	Bornology.isBounded_compl_iff
inter 📖	mathematical	Bornology.IsCobounded	Set Set.instInter	—	Bornology.isCobounded_inter
of_compl 📖	mathematical	Bornology.IsCobounded Compl.compl Set Set.instCompl	Bornology.IsBounded	—	Bornology.isCobounded_compl_iff
superset 📖	—	Bornology.IsCobounded Set Set.instHasSubset	—	—	Filter.mem_of_superset

BoundedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounded_univ 📖	mathematical	—	Bornology.IsBounded Set.univ	—	—
of_finite 📖	mathematical	—	BoundedSpace	—	Set.Finite.isBounded Set.toFinite Subtype.finite

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_cobounded_iff 📖	mathematical	Filter.HasBasis	Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter Bornology.cobounded Bornology.IsBounded	—	disjoint_iff_left

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_ne_cobounded 📖	mathematical	Filter.Tendsto Bornology.cobounded	Filter.Eventually	—	eventually Bornology.eventually_ne_cobounded

OrderDual

Definitions

Name	Category	Theorems
instBornology 📖	CompOp	4 math math: isBounded_preimage_toDual, isBounded_preimage_ofDual, isCobounded_preimage_ofDual, isCobounded_preimage_toDual

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_preimage_ofDual 📖	mathematical	—	Bornology.IsBounded OrderDual instBornology Set.preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofDual	—	—
isBounded_preimage_toDual 📖	mathematical	—	Bornology.IsBounded Set.preimage OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual instBornology	—	—
isCobounded_preimage_ofDual 📖	mathematical	—	Bornology.IsCobounded OrderDual instBornology Set.preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofDual	—	—
isCobounded_preimage_toDual 📖	mathematical	—	Bornology.IsCobounded Set.preimage OrderDual DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toDual instBornology	—	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded 📖	mathematical	—	Bornology.IsBounded	—	Bornology.le_cofinite compl_mem_cofinite

(root)

Definitions

Name	Category	Theorems
BoundedSpace 📖	CompData	21 math math: BoundedSpace.of_finite, UniformOnFun.instBoundedSpace, Bornology.IsBounded.boundedSpace_subtype, Tactic.ComputeAsymptotics.Seq.instBoundedSpaceSeq, Bornology.IsBounded.boundedSpace_val, Metric.boundedSpace_iff, boundedSpace_subtype_iff, PiNat.boundedSpace, instBoundedSpaceProd, UniformFun.instBoundedSpace, boundedSpace_val_set_iff, Bornology.cobounded_eq_bot_iff, Bornology.isBounded_univ, Tactic.ComputeAsymptotics.Seq.instBoundedSpaceStream', Metric.boundedSpace_iff_nndist, instBoundedSpaceAdditive, instBoundedSpaceOrderDual, instBoundedSpaceSubtype, instBoundedSpaceMultiplicative, boundedSpace_induced_iff, Metric.boundedSpace_iff_edist
instBornologyPUnit 📖	CompOp	—

---

← Back to Index