Absorbs

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

Statistics

Metric	Count
Definitions Absorbent, Absorbs, absorbing	3
Theorems absorbs, absorbs_finite, mono, vadd_absorbs, zero_mem, add, biInter, biUnion, biUnion_finset, empty, eventually, iInter, iUnion, inter, mono, mono_left, mono_right, neg_neg, of_boundedSpace, of_neg_neg, restrict_scalars, sInter, sUnion, sub, union, univ, zero, mem_absorbing, absorbs_biInter, absorbs_biUnion, absorbs_sInter, absorbs_sUnion, absorbent_iff_forall_absorbs_singleton, absorbent_iff_inv_smul, absorbent_univ, absorbs_biUnion_finset, absorbs_iInter, absorbs_iUnion, absorbs_iff_eventually_cobounded_mapsTo, absorbs_inter, absorbs_neg_neg, absorbs_union, absorbs_zero_iff, eventually_cobounded_mapsTo	44
Total	47

Absorbent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absorbs 📖	mathematical	Absorbent	Absorbs Set Set.instSingletonSet	—	—
absorbs_finite 📖	mathematical	Absorbent	Absorbs	—	Set.biUnion_of_singleton Absorbs.biUnion absorbs
mono 📖	—	Absorbent Set Set.instHasSubset	—	—	Absorbs.mono_left
vadd_absorbs 📖	mathematical	Absorbent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass Absorbs	Set Set.add AddZero.toAdd HVAdd.hVAdd instHVAdd Set.vaddSet Add.toVAdd	—	Set.singleton_vadd Absorbs.add
zero_mem 📖	mathematical	Absorbent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	Set Set.instMembership	—	absorbs_zero_iff

Absorbs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass	Set Set.add AddZero.toAdd	—	Filter.Eventually.mp Filter.Eventually.mono eventually smul_add Set.add_subset_add
biInter 📖	mathematical	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	Set.iInter Set Set.instMembership	—	Set.Finite.absorbs_biInter
biUnion 📖	mathematical	Absorbs	Set.iUnion Set Set.instMembership	—	Set.Finite.absorbs_biUnion
biUnion_finset 📖	mathematical	Absorbs	Set.iUnion Finset Finset.instMembership	—	absorbs_biUnion_finset
empty 📖	mathematical	—	Absorbs Set Set.instEmptyCollection	—	—
eventually 📖	mathematical	Absorbs	Filter.Eventually Set Set.instHasSubset Set.smulSet Bornology.cobounded	—	—
iInter 📖	mathematical	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	Set.iInter	—	absorbs_iInter
iUnion 📖	mathematical	Absorbs	Set.iUnion	—	absorbs_iUnion
inter 📖	mathematical	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	Set Set.instInter	—	absorbs_inter
mono 📖	—	Absorbs Set Set.instHasSubset	—	—	mono_right mono_left
mono_left 📖	—	Absorbs Set Set.instHasSubset	—	—	Filter.Eventually.mono HasSubset.Subset.trans Set.instIsTransSubset Set.smul_set_mono
mono_right 📖	—	Absorbs Set Set.instHasSubset	—	—	Filter.Eventually.mono HasSubset.Subset.trans Set.instIsTransSubset
neg_neg 📖	mathematical	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	absorbs_neg_neg
of_boundedSpace 📖	mathematical	—	Absorbs	—	Bornology.cobounded_eq_bot
of_neg_neg 📖	—	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—	absorbs_neg_neg
restrict_scalars 📖	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction Filter.Tendsto MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass Bornology.cobounded	—	—	Filter.Eventually.mono Filter.Tendsto.eventually smul_one_smul Set.isScalarTower
sInter 📖	mathematical	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	Set.sInter	—	Set.Finite.absorbs_sInter
sUnion 📖	mathematical	Absorbs	Set.sUnion	—	Set.Finite.absorbs_sUnion
sub 📖	mathematical	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Set Set.sub SubNegMonoid.toSub	—	sub_eq_add_neg add neg_neg
union 📖	mathematical	Absorbs	Set Set.instUnion	—	absorbs_union
univ 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set.univ	—	Filter.Eventually.mono Bornology.eventually_ne_cobounded Set.smul_set_univ₀ Set.subset_univ
zero 📖	mathematical	Set Set.instMembership	Absorbs SMulZeroClass.toSMul Set.zero	—	Filter.Eventually.of_forall Set.zero_subset Set.zero_mem_smul_set

Filter

Definitions

Name	Category	Theorems
absorbing 📖	CompOp	2 math math: mem_absorbing, Bornology.isVonNBounded_iff_absorbing_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_absorbing 📖	mathematical	—	Set Filter instMembership absorbing Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	—	—

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absorbs_biInter 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set.iInter Set Set.instMembership	—	Filter.biInter_mem
absorbs_biUnion 📖	mathematical	—	Absorbs Set.iUnion Set Set.instMembership	—	—
absorbs_sInter 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set.sInter	—	Filter.sInter_mem
absorbs_sUnion 📖	mathematical	—	Absorbs Set.sUnion	—	—

(root)

Definitions

Name	Category	Theorems
Absorbent 📖	MathDef	11 math math: absorbent_iff_eventually_nhdsNE_zero, Seminorm.absorbent_closedBall_zero, absorbent_univ, absorbent_nhds_zero, Seminorm.absorbent_ball_zero, absorbent_ball, absorbent_iff_forall_absorbs_singleton, Seminorm.absorbent_closedBall, absorbent_iff_inv_smul, Seminorm.absorbent_ball, absorbent_ball_zero
Absorbs 📖	MathDef	28 math math: absorbs_zero_iff, Filter.mem_absorbing, Absorbs.empty, Absorbent.absorbs, absorbs_inter, absorbs_biUnion_finset, Set.Finite.absorbs_sInter, Absorbs.of_boundedSpace, absorbs_iff_eventually_nhdsNE_zero, absorbs_iUnion, Bornology.isVonNBounded_iff, absorbs_iInter, absorbs_union, absorbs_iff_eventually_cobounded_mapsTo, Set.Finite.absorbs_biUnion, absorbs_iff_norm, Balanced.absorbs_self, Seminorm.ball_zero_absorbs_ball_zero, absorbent_iff_forall_absorbs_singleton, Absorbs.zero, Filter.HasBasis.isVonNBounded_iff, Absorbent.absorbs_finite, absorbs_iff_eventually_nhds_zero, Absorbs.of_norm, Absorbs.univ, Set.Finite.absorbs_biInter, absorbs_neg_neg, Set.Finite.absorbs_sUnion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absorbent_iff_forall_absorbs_singleton 📖	mathematical	—	Absorbent Absorbs Set Set.instSingletonSet	—	—
absorbent_iff_inv_smul 📖	mathematical	—	Absorbent SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Filter.Eventually Set Set.instMembership InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Bornology.cobounded	—	—
absorbent_univ 📖	mathematical	—	Absorbent SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set.univ	—	Absorbs.univ
absorbs_biUnion_finset 📖	mathematical	—	Absorbs Set.iUnion Finset Finset.instMembership	—	Set.Finite.absorbs_biUnion Finset.finite_toSet
absorbs_iInter 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set.iInter	—	Filter.iInter_mem
absorbs_iUnion 📖	mathematical	—	Absorbs Set.iUnion	—	Set.Finite.absorbs_sUnion Set.finite_range Set.forall_mem_range
absorbs_iff_eventually_cobounded_mapsTo 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Filter.Eventually Set.MapsTo InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Bornology.cobounded	—	Filter.eventually_congr Filter.Eventually.mono Bornology.eventually_ne_cobounded Set.preimage_smul_inv₀
absorbs_inter 📖	mathematical	—	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction Set Set.instInter	—	—
absorbs_neg_neg 📖	mathematical	—	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Set.smul_set_neg
absorbs_union 📖	mathematical	—	Absorbs Set Set.instUnion	—	—
absorbs_zero_iff 📖	mathematical	—	Absorbs SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero Set Set.zero Set.instMembership	—	smul_zero
eventually_cobounded_mapsTo 📖	mathematical	Absorbs SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero MulAction.toSemigroupAction	Filter.Eventually Set.MapsTo InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid Bornology.cobounded	—	absorbs_iff_eventually_cobounded_mapsTo

---

← Back to Index