ContinuousOfBounded

📁 Source: Mathlib/Analysis/LocallyConvex/ContinuousOfBounded.lean

Statistics

Metric	Count
Definitions clmOfExistsBoundedImage	1
Theorems clmOfExistsBoundedImage_apply, clmOfExistsBoundedImage_coe, continuousAt_zero_of_locally_bounded, continuous_of_locally_bounded	4
Total	5

LinearMap

Definitions

Name	Category	Theorems
clmOfExistsBoundedImage 📖	CompOp	2 math math: clmOfExistsBoundedImage_apply, clmOfExistsBoundedImage_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
clmOfExistsBoundedImage_apply 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing 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 NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Set.image DFunLike.coe LinearMap NontriviallyNormedField.toNormedField instFunLike	ContinuousLinearMap ContinuousLinearMap.funLike clmOfExistsBoundedImage	—	—
clmOfExistsBoundedImage_coe 📖	mathematical	Set Filter Filter.instMembership nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing 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 NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Set.image DFunLike.coe LinearMap NontriviallyNormedField.toNormedField instFunLike	ContinuousLinearMap.toLinearMap clmOfExistsBoundedImage	—	—
continuousAt_zero_of_locally_bounded 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing 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 NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image DFunLike.coe LinearMap NontriviallyNormedField.toNormedField instFunLike	ContinuousAt	—	NormedField.exists_norm_lt_one norm_pos_iff Filter.HasBasis.exists_antitone_subbasis FirstCountableTopology.nhds_generated_countable nhds_basis_balanced NormedField.nhdsNE_neBot Filter.HasBasis.to_hasBasis' Filter.HasAntitoneBasis.toHasBasis norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass le_imp_le_of_le_of_le pow_le_pow_left₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt le_refl one_pow smul_zero smul_mem_nhds_smul₀ ContinuousSMul.continuousConstSMul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass Filter.HasBasis.tendsto_left_iff Mathlib.Tactic.Push.not_forall_eq Filter.HasAntitoneBasis.tendsto Set.mem_smul_set_iff_inv_smul_mem₀ Filter.Tendsto.isVonNBounded_range tendsto_pow_atTop_nhds_zero_of_norm_lt_one RingHomIsometric.norm_map Bornology.IsVonNBounded.smul_tendsto_zero map_smulₛₗ map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass Filter.Eventually.of_forall Set.mem_range_self Filter.Tendsto.congr smul_inv_smul₀ IsSimpleRing.instNontrivial DivisionRing.isSimpleRing Filter.frequently_false Filter.Eventually.frequently Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.mp_mem Filter.Tendsto.eventually_mem Filter.univ_mem'
continuous_of_locally_bounded 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing 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 NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.image DFunLike.coe LinearMap NontriviallyNormedField.toNormedField instFunLike	Continuous	—	continuous_of_continuousAt_zero IsTopologicalAddGroup.toContinuousAdd DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass continuousAt_zero_of_locally_bounded

---

← Back to Index