Seq

📁 Source: Mathlib/Analysis/Calculus/TangentCone/Seq.lean

Statistics

Metric	Count
Definitions	0
Theorems mem_tangentConeAt_iff_exists_seq, mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop, mem_tangentConeAt_of_pow_smul, lim_zero	4
Total	4

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_tangentConeAt_iff_exists_seq 📖	mathematical	—	Set Set.instMembership tangentConeAt Filter.Tendsto Filter.atTop Nat.instPreorder nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Filter.Eventually AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	Filter.exists_seq_tendsto Filter.Inf.isCountablyGenerated Filter.comap.isCountablyGenerated FirstCountableTopology.nhds_generated_countable Filter.prod.isCountablyGenerated Filter.isCountablyGenerated_top TopologicalSpace.isCountablyGenerated_nhdsWithin tangentConeAt_def mem_tangentConeAt_of_seq Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop 📖	mathematical	—	Set Set.instMembership tangentConeAt NormedAddCommGroup.toAddCommGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Filter.Tendsto Real Norm.norm NormedField.toNorm Filter.atTop Nat.instPreorder Real.instPreorder Filter.Eventually AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup nhds	—	eq_or_ne zero_mem_tangentConeAt_iff IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup NormedField.exists_lt_norm Nat.instAtLeastTwoHAddOfNat Metric.mem_closure_iff pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_pos Mathlib.Meta.NormNum.instAtLeastTwo lt_trans add_sub_cancel one_div mul_inv_rev dist_eq_norm_sub' norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean Filter.Eventually.of_forall Filter.HasBasis.tendsto_iff Filter.atTop_basis instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Metric.nhds_basis_ball_pow one_half_pos one_half_lt_one lt_div_iff₀' LT.lt.trans_le le_imp_le_of_le_of_le le_refl div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_le_div₀ le_of_lt pow_le_pow_right₀ Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Mathlib.Meta.NormNum.isNat_le_true Set.mem_Ici div_eq_inv_mul mul_one mul_pow inv_pow dist_zero_right norm_smul NormedSpace.toNormSMulClass mem_tangentConeAt_iff_exists_seq TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.Tendsto.norm Filter.Eventually.mono Filter.Tendsto.eventually_ne T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace right_ne_zero_of_smul Filter.Tendsto.num instOrderTopologyReal inv_nhdsGT_zero Filter.comap_inv Filter.tendsto_comap_iff inv_inv norm_zero mem_tangentConeAt_of_seq Filter.atTop_neBot tangentConeAt.lim_zero IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul
mem_tangentConeAt_of_pow_smul 📖	mathematical	Real Real.instLT Norm.norm NormedDivisionRing.toNorm Real.instOne Filter.Eventually Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction Monoid.toNatPow Filter.atTop Nat.instPreorder	tangentConeAt	—	mem_tangentConeAt_of_add_smul_mem Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_nhdsWithin_iff tendsto_pow_atTop_nhds_zero_of_norm_lt_one isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass IsSimpleRing.instNontrivial DivisionRing.isSimpleRing

tangentConeAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lim_zero 📖	mathematical	Filter.Tendsto Real Norm.norm NormedDivisionRing.toNorm Filter.atTop Real.instPreorder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid nhds	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Filter.Eventually.mono eventually_ne_of_tendsto_norm_atTop inv_smul_smul₀ zero_smul Filter.Tendsto.congr' Filter.Tendsto.smul Filter.Tendsto.comp Filter.tendsto_inv₀_cobounded tendsto_norm_atTop_iff_cobounded

---

← Back to Index