Bounded

📁 Source: Mathlib/Topology/Algebra/Module/Multilinear/Bounded.lean

Statistics

Metric	Count
Definitions	0
Theorems image_multilinear, image_multilinear'	2
Total	2

Bornology.IsVonNBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_multilinear 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Pi.instZero Pi.topologicalSpace	AddZero.toZero AddZeroClass.toAddZero Set.image DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike	—	isEmpty_or_nonempty Bornology.isBounded_iff_isVonNBounded Set.Finite.isBounded Set.Finite.image Set.toFinite Subtype.finite Finite.of_fintype image_multilinear'
image_multilinear' 📖	mathematical	Bornology.IsVonNBounded SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid Pi.instZero Pi.topologicalSpace	AddZero.toZero AddZeroClass.toAddZero Set.image DFunLike.coe ContinuousMultilinearMap ContinuousMultilinearMap.funLike	—	absorbs_iff_norm Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Continuous.tendsto' ContinuousMapClass.map_continuous ContinuousMultilinearMap.continuousMapClass ContinuousMultilinearMap.map_zero Set.exists_finite_iff_finset Filter.mem_pi nhds_pi Filter.Tendsto.eventually tendsto_smallSets_nhds Bornology.isVonNBounded_pi_iff Filter.mem_lift' Filter.HasBasis.eventually_iff NormedAddCommGroup.nhds_zero_basis_norm_lt NormedField.exists_norm_lt norm_pos_iff LE.le.trans_lt absorbs_iff_eventually_nhds_zero mem_of_mem_nhds Finset.prod_ne_zero_iff IsSimpleRing.instNontrivial DivisionRing.isSimpleRing NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Set.mapsTo_image_iff eq_or_ne Function.update_self Finset.piecewise_eq_of_mem smul_smul norm_mul norm_div mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono LT.lt.le Membership.mem.out le_of_lt norm_nonneg div_self_le_one Real.instZeroLEOneClass one_mul Function.update_of_ne le_rfl ContinuousMultilinearMap.map_update_smul Function.update_eq_self ContinuousMultilinearMap.map_piecewise_smul div_eq_mul_inv SemigroupAction.mul_smul inv_smul_smul₀

---

← Back to Index