Documentation Verification Report

AsymptoticCone

📁 Source: Mathlib/Topology/Algebra/AsymptoticCone.lean

Statistics

Metric	Count
Definitions `asymptoticNhds`, `asymptoticCone`	2
Theorems `asymptoticNhds_bind_asymptoticNhds`, `asymptoticNhds_bind_nhds`, `asymptoticNhds_eq_smul`, `asymptoticNhds_eq_smul_vadd`, `asymptoticNhds_smul`, `asymptoticNhds_vadd_pure`, `asymptoticNhds_zero`, `instNeBotAsymptoticNhds`, `nhds_bind_asymptoticNhds`, `vadd_asymptoticNhds`, `asymptoticCone`, `smul_vadd_mem_of_isClosed_of_mem_asymptoticCone`, `smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone`, `asymptoticNhds_vadd_const`, `atTop_smul_const_tendsto_asymptoticNhds`, `atTop_smul_nhds_tendsto_asymptoticNhds`, `const_vadd_asymptoticNhds`, `asymptoticCone_biUnion`, `smul_vadd_mem_of_isClosed_of_mem_asymptoticCone`, `asymptoticCone_affineSubspace`, `asymptoticCone_asymptoticCone`, `asymptoticCone_biUnion`, `asymptoticCone_closure`, `asymptoticCone_empty`, `asymptoticCone_eq_closure_of_forall_smul_mem`, `asymptoticCone_iUnion_of_finite`, `asymptoticCone_mono`, `asymptoticCone_nonempty`, `asymptoticCone_sUnion`, `asymptoticCone_submodule`, `asymptoticCone_union`, `asymptoticCone_univ`, `isClosed_asymptoticCone`, `mem_asymptoticCone_iff`, `smul_mem_asymptoticCone`, `smul_mem_asymptoticCone_iff`, `zero_mem_asymptoticCone`	37
Total	39

AffineSpace

Definitions

Name	Category	Theorems
`asymptoticNhds` 📖	CompOp	15 math math: `asymptoticNhds_smul`, `cobounded_eq_iSup_sphere_asymptoticNhds`, `asymptoticNhds_bind_asymptoticNhds`, `asymptoticNhds_vadd_pure`, `Filter.Tendsto.atTop_smul_nhds_tendsto_asymptoticNhds`, `instNeBotAsymptoticNhds`, `nhds_bind_asymptoticNhds`, `asymptoticNhds_zero`, `vadd_asymptoticNhds`, `Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds`, `asymptoticNhds_le_cobounded`, `mem_asymptoticCone_iff`, `asymptoticNhds_eq_smul`, `asymptoticNhds_eq_smul_vadd`, `asymptoticNhds_bind_nhds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticNhds_bind_asymptoticNhds` 📖	mathematical	—	`Filter.bind` `asymptoticNhds` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	—	`Filter.ext'` `asymptoticNhds_eq_smul` `Filter.eventually_bind` `Filter.map₂_smul` `Filter.map_prod_eq_map₂` `Filter.eventually_map` `nhds_bind_asymptoticNhds` `Filter.map_snd_prod` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `Filter.eventually_congr` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.tendsto_fst` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Filter.univ_mem'` `asymptoticNhds_smul`
`asymptoticNhds_bind_nhds` 📖	mathematical	—	`Filter.bind` `asymptoticNhds` `nhds`	—	`le_antisymm` `AddTorsor.nonempty` `asymptoticNhds_eq_smul_vadd` `Filter.vadd_pure` `nhds_bind_nhds` `Filter.mem_bind` `Filter.bind_map` `Filter.smul_mem_smul` `Filter.inter_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `EuclideanDomain.toNontrivial` `Set.forall_mem_image2` `Set.preimage_preimage` `vsub_vadd` `Filter.Tendsto.vsub` `Filter.tendsto_id` `tendsto_const_nhds` `vadd_vsub` `Filter.mp_mem` `smul_mem_nhds_smul₀` `ContinuousSMul.continuousConstSMul` `LT.lt.ne'` `Filter.univ_mem'` `Set.image_smul` `Set.forall_mem_image` `Set.smul_mem_smul` `Filter.bind_mono` `le_rfl` `Filter.Eventually.of_forall` `pure_le_nhds`
`asymptoticNhds_eq_smul` 📖	mathematical	—	`asymptoticNhds` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `Filter` `Filter.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	—	`le_antisymm` `iSup_le` `Filter.add_pure` `Filter.map_map₂` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.tendsto_fst` `Filter.eventually_ne_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `EuclideanDomain.toNontrivial` `Filter.univ_mem'` `smul_add` `smul_inv_smul₀` `Filter.map_congr` `Filter.map_map` `Filter.map_mono` `Filter.Tendsto.prodMk` `Filter.Tendsto.add` `IsTopologicalAddGroup.toContinuousAdd` `Filter.tendsto_snd` `Filter.Tendsto.smul_const` `Filter.Tendsto.inv_tendsto_atTop` `zero_smul` `add_zero` `LE.le.trans'` `le_iSup`
`asymptoticNhds_eq_smul_vadd` 📖	mathematical	—	`asymptoticNhds` `HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `Filter.instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds` `Filter.instPure`	—	`asymptoticNhds_eq_smul` `asymptoticNhds_vadd_pure`
`asymptoticNhds_smul` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`asymptoticNhds` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`AddTorsor.nonempty` `asymptoticNhds_eq_smul_vadd` `Homeomorph.map_nhds_eq` `ContinuousSMul.continuousConstSMul` `LT.lt.ne'` `Filter.map₂_map_right` `smul_smul` `OrderIso.map_atTop` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono`
`asymptoticNhds_vadd_pure` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `asymptoticNhds` `addGroupIsAddTorsor` `Filter.instPure`	—	`asymptoticNhds.eq_1` `Filter.vadd_pure` `Filter.map_iSup` `Filter.map_map` `Equiv.iSup_congr` `AddSemigroupAction.add_vadd`
`asymptoticNhds_zero` 📖	mathematical	—	`asymptoticNhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Top.top` `Filter` `Filter.instTop`	—	`AddTorsor.nonempty` `asymptoticNhds_vadd_pure` `Filter.vadd_pure` `Function.Surjective.filter_map_top` `Equiv.surjective`
`instNeBotAsymptoticNhds` 📖	mathematical	—	`Filter.NeBot` `asymptoticNhds`	—	`AddTorsor.nonempty` `asymptoticNhds_eq_smul_vadd` `Filter.vadd.instNeBot` `Filter.smul.instNeBot` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `nhds_neBot` `Filter.pure_neBot`
`nhds_bind_asymptoticNhds` 📖	mathematical	—	`Filter.bind` `nhds` `asymptoticNhds`	—	`le_antisymm` `AddTorsor.nonempty` `asymptoticNhds_eq_smul_vadd` `Filter.vadd_pure` `nhds_bind_nhds` `Filter.pure_bind` `Filter.bind_mono` `pure_le_nhds` `Filter.EventuallyLE.rfl`
`vadd_asymptoticNhds` 📖	mathematical	—	`HVAdd.hVAdd` `Filter` `instHVAdd` `Filter.instVAddFilter` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction` `asymptoticNhds`	—	`AddTorsor.nonempty` `asymptoticNhds_vadd_pure` `Filter.vadd_pure` `Filter.map_map` `VAddCommClass.vadd_comm` `vaddCommClass_self`

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticCone` 📖	mathematical	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`asymptoticCone` `addGroupIsAddTorsor`	—	`Set.eq_empty_or_nonempty` `asymptoticCone_empty` `convex_empty` `mem_asymptoticCone_iff` `Filter.Tendsto.frequently` `Filter.Tendsto.asymptoticNhds_vadd_const` `Filter.Tendsto.atTop_smul_const_tendsto_asymptoticNhds` `Filter.tendsto_id` `Filter.Eventually.frequently` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `smul_add` `smul_smul` `smul_vadd_mem_of_isClosed_of_mem_asymptoticCone` `segment_subset` `affineSegment_eq_segment` `IsStrictOrderedRing.toIsOrderedRing` `mem_vadd_const_affineSegment` `Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval` `Mathlib.Tactic.Module.NF.add_eq_eval` `Mathlib.Tactic.Module.NF.smul_eq_eval` `Mathlib.Tactic.Module.NF.atom_eq_eval` `Mathlib.Tactic.Module.NF.eval_algebraMap` `AddCommMonoid.nat_isScalarTower` `Mathlib.Tactic.Module.NF.add_eq_eval₁` `zero_add` `Mathlib.Tactic.Module.NF.eq_cons_cons` `eq_natCast` `RingHom.instRingHomClass` `Nat.cast_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `asymptoticCone_closure` `instIsTopologicalAddTorsor` `closure` `ContinuousSMul.continuousConstSMul` `isClosed_closure`
`smul_vadd_mem_of_isClosed_of_mem_asymptoticCone` 📖	mathematical	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set` `Set.instMembership` `asymptoticCone` `addGroupIsAddTorsor`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`StarConvex.smul_vadd_mem_of_isClosed_of_mem_asymptoticCone`
`smul_vadd_mem_of_mem_nhds_of_mem_asymptoticCone` 📖	mathematical	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `asymptoticCone` `addGroupIsAddTorsor`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`Filter.frequently_const` `Filter.prod.instNeBot` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `nhds_neBot` `Filter.Frequently.mp` `Filter.frequently_map` `Filter.map_prod_eq_map₂` `Filter.map₂_smul` `Filter.vadd_pure` `AffineSpace.asymptoticNhds_eq_smul_vadd` `mem_asymptoticCone_iff` `Continuous.tendsto'` `Continuous.vadd` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor` `Continuous.neg` `IsTopologicalAddGroup.toContinuousNeg` `Continuous.const_smul` `ContinuousSMul.continuousConstSMul` `continuous_id'` `continuous_const` `neg_add_cancel_left` `Filter.mp_mem` `Filter.Tendsto.comp` `Filter.tendsto_snd` `Filter.Tendsto.eventually` `Filter.tendsto_fst` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Filter.univ_mem'` `segment_subset` `vsub_vadd_eq_vsub_sub` `vsub_self` `zero_sub` `neg_neg` `vadd_vsub` `SameRay.pos_smul_right` `PosSMulMono.toSMulPosMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `SameRay.sameRay_nonneg_smul_left`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticNhds_vadd_const` 📖	mathematical	`Filter.Tendsto` `AffineSpace.asymptoticNhds` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`AffineSpace.asymptoticNhds_vadd_pure` `Filter.vadd_pure` `comp` `Filter.tendsto_map`
`atTop_smul_const_tendsto_asymptoticNhds` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AffineSpace.asymptoticNhds` `addGroupIsAddTorsor`	—	`atTop_smul_nhds_tendsto_asymptoticNhds` `tendsto_const_nhds`
`atTop_smul_nhds_tendsto_asymptoticNhds` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `nhds`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AffineSpace.asymptoticNhds` `addGroupIsAddTorsor`	—	`AffineSpace.asymptoticNhds_eq_smul` `Filter.map₂_smul` `Filter.map_prod_eq_map₂` `comp` `Filter.tendsto_map` `prodMk`
`const_vadd_asymptoticNhds` 📖	mathematical	`Filter.Tendsto` `AffineSpace.asymptoticNhds`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`AffineSpace.vadd_asymptoticNhds` `Filter.map_vadd` `comp` `Filter.tendsto_map`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticCone_biUnion` 📖	mathematical	—	`asymptoticCone` `Set.iUnion` `Finset` `instMembership`	—	`asymptoticCone_biUnion` `finite_toSet`

StarConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_vadd_mem_of_isClosed_of_mem_asymptoticCone` 📖	mathematical	`StarConvex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Preorder.toLE` `PartialOrder.toPreorder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set` `Set.instMembership` `asymptoticCone` `addGroupIsAddTorsor`	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddTorsor.toAddAction`	—	`isClosed_iff_frequently` `Filter.Tendsto.frequently` `Filter.Tendsto.vadd_const` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor` `Filter.Tendsto.const_smul` `ContinuousSMul.continuousConstSMul` `Filter.tendsto_snd` `Filter.Frequently.mp` `Filter.frequently_map` `Filter.map_prod_eq_map₂` `Filter.map₂_smul` `Filter.vadd_pure` `AffineSpace.asymptoticNhds_eq_smul_vadd` `mem_asymptoticCone_iff` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.tendsto_fst` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `segment_subset` `SameRay.congr_simp` `vadd_vsub` `vadd_vsub_vadd_cancel_right` `SameRay.nonneg_smul_right` `PosSMulMono.toSMulPosMono` `IsStrictOrderedRing.toIsOrderedRing` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedModule.toPosSMulMono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `IsScalarTower.left` `SameRay.sameRay_nonneg_smul_left` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`

(root)

Definitions

Name	Category	Theorems
`asymptoticCone` 📖	CompOp	22 math math: `not_bounded_iff_exists_ne_zero_mem_asymptoticCone`, `asymptoticCone_empty`, `asymptoticCone_asymptoticCone`, `isBounded_iff_asymptoticCone_subset_singleton`, `asymptoticCone_affineSubspace`, `Finset.asymptoticCone_biUnion`, `asymptoticCone_iUnion_of_finite`, `zero_mem_asymptoticCone`, `asymptoticCone_biUnion`, `asymptoticCone_sUnion`, `asymptoticCone_union`, `isClosed_asymptoticCone`, `asymptoticCone_closure`, `asymptoticCone_nonempty`, `mem_asymptoticCone_iff`, `asymptoticCone_subset_singleton_of_bounded`, `smul_mem_asymptoticCone_iff`, `asymptoticCone_submodule`, `asymptoticCone_mono`, `asymptoticCone_eq_closure_of_forall_smul_mem`, `asymptoticCone_univ`, `Convex.asymptoticCone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`asymptoticCone_affineSubspace` 📖	mathematical	`Set.Nonempty` `SetLike.coe` `AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `AffineSubspace.instSetLike`	`asymptoticCone` `closure` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `AffineSubspace.direction`	—	`Set.ext` `AffineSpace.asymptoticNhds_vadd_pure` `Filter.vadd_pure` `AffineSubspace.vadd_mem_iff_mem_direction`
`asymptoticCone_asymptoticCone` 📖	mathematical	—	`asymptoticCone` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup`	—	`Set.ext` `AffineSpace.asymptoticNhds_bind_asymptoticNhds`
`asymptoticCone_biUnion` 📖	mathematical	—	`asymptoticCone` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.Finite.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `asymptoticCone_empty` `Set.iUnion_iUnion_eq_or_left` `asymptoticCone_union`
`asymptoticCone_closure` 📖	mathematical	—	`asymptoticCone` `closure`	—	`Set.ext` `AffineSpace.asymptoticNhds_bind_nhds`
`asymptoticCone_empty` 📖	mathematical	—	`asymptoticCone` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_iff_forall_notMem` `Filter.frequently_false`
`asymptoticCone_eq_closure_of_forall_smul_mem` 📖	mathematical	`Set` `Set.instMembership` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	`asymptoticCone` `addGroupIsAddTorsor` `closure`	—	`Set.ext` `mem_closure_iff_frequently` `Filter.map_snd_prod` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `Filter.frequently_map` `mem_asymptoticCone_iff` `AffineSpace.asymptoticNhds_eq_smul` `Filter.map₂_smul` `Filter.map_prod_eq_map₂` `Filter.frequently_congr` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.tendsto_fst` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `IsStrictOrderedRing.toIsOrderedRing` `Filter.univ_mem'` `inv_smul_smul₀` `LT.lt.ne'` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono`
`asymptoticCone_iUnion_of_finite` 📖	mathematical	—	`asymptoticCone` `Set.iUnion`	—	`Set.sUnion_range` `asymptoticCone_sUnion` `Set.finite_range` `Set.biUnion_range`
`asymptoticCone_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`asymptoticCone`	—	`Filter.Frequently.mono`
`asymptoticCone_nonempty` 📖	mathematical	—	`Set.Nonempty` `asymptoticCone`	—	`Function.mtr` `asymptoticCone_empty` `zero_mem_asymptoticCone`
`asymptoticCone_sUnion` 📖	mathematical	—	`asymptoticCone` `Set.sUnion` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.sUnion_eq_biUnion` `asymptoticCone_biUnion`
`asymptoticCone_submodule` 📖	mathematical	—	`asymptoticCone` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `SetLike.coe` `Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `closure`	—	`asymptoticCone_eq_closure_of_forall_smul_mem` `Submodule.smul_mem`
`asymptoticCone_union` 📖	mathematical	—	`asymptoticCone` `Set` `Set.instUnion`	—	`Set.ext`
`asymptoticCone_univ` 📖	mathematical	—	`asymptoticCone` `Set.univ`	—	`AffineSubspace.top_coe` `asymptoticCone_affineSubspace` `Set.univ_nonempty` `AddTorsor.nonempty` `AffineSubspace.direction_top` `Submodule.top_coe` `closure_univ`
`isClosed_asymptoticCone` 📖	mathematical	—	`IsClosed` `asymptoticCone`	—	`AddTorsor.nonempty` `isClosed_iff_frequently` `AffineSpace.nhds_bind_asymptoticNhds`
`mem_asymptoticCone_iff` 📖	mathematical	—	`Set` `Set.instMembership` `asymptoticCone` `Filter.Frequently` `AffineSpace.asymptoticNhds`	—	—
`smul_mem_asymptoticCone` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set` `Set.instMembership` `asymptoticCone`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`LE.le.eq_or_lt` `zero_smul` `zero_mem_asymptoticCone` `asymptoticCone_nonempty` `smul_mem_asymptoticCone_iff`
`smul_mem_asymptoticCone_iff` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Set` `Set.instMembership` `asymptoticCone` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`AffineSpace.asymptoticNhds_smul`
`zero_mem_asymptoticCone` 📖	mathematical	—	`Set` `Set.instMembership` `asymptoticCone` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.Nonempty`	—	`Function.mtr` `asymptoticCone_empty` `AffineSpace.asymptoticNhds_zero`

---

← Back to Index