SeminormFromBounded

📁 Source: Mathlib/Analysis/Normed/Unbundled/SeminormFromBounded.lean

Statistics

Metric	Count
Definitions normFromBounded, seminormFromBounded, seminormFromBounded'	3
Theorems map_mul_zero_of_map_zero, map_one_ne_zero, map_pow_ne_zero, seminormFromBounded_add, seminormFromBounded_aux, seminormFromBounded_bddAbove_range, seminormFromBounded_eq_zero_iff, seminormFromBounded_ge, seminormFromBounded_isNonarchimedean, seminormFromBounded_is_norm_iff, seminormFromBounded_ker, seminormFromBounded_le, seminormFromBounded_mul, seminormFromBounded_neg, seminormFromBounded_nonneg, seminormFromBounded_nonzero, seminormFromBounded_of_mul_apply, seminormFromBounded_of_mul_is_mul, seminormFromBounded_of_mul_le, seminormFromBounded_one, seminormFromBounded_one_le, seminormFromBounded_zero	22
Total	25

(root)

Definitions

Name	Category	Theorems
normFromBounded 📖	CompOp	—
seminormFromBounded 📖	CompOp	—
seminormFromBounded' 📖	CompOp	15 math math: seminormFromBounded_ker, seminormFromBounded_of_mul_is_mul, seminormFromBounded_zero, seminormFromBounded_one_le, seminormFromBounded_of_mul_apply, seminormFromBounded_of_mul_le, seminormFromBounded_le, seminormFromBounded_neg, seminormFromBounded_eq_zero_iff, seminormFromBounded_one, seminormFromBounded_isNonarchimedean, seminormFromBounded_mul, seminormFromBounded_nonneg, seminormFromBounded_add, seminormFromBounded_ge

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mul_zero_of_map_zero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	MulZeroClass.mul_zero MulZeroClass.zero_mul le_antisymm
map_one_ne_zero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	Function.ne_iff LE.le.antisymm MulZeroClass.zero_mul MulZeroClass.mul_zero one_mul
map_pow_ne_zero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	map_one_ne_zero Function.ne_iff IsUnit.mul_val_inv one_pow MulZeroClass.mul_zero MulZeroClass.zero_mul LE.le.antisymm
seminormFromBounded_add 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul Distrib.toAdd Real.instAdd	seminormFromBounded'	—	ciSup_le AddTorsor.nonempty div_zero zero_add add_div div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' add_mul Distrib.rightDistribClass le_trans add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_ciSup_of_le seminormFromBounded_bddAbove_range le_refl
seminormFromBounded_aux 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	LE.le.eq_or_lt' MulZeroClass.mul_zero le_of_not_gt 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.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add 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 le_mul_iff_one_le_left IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul mul_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.sub_subst div_le_iff₀ MulPosReflectLE.toMulPosReflectLT Mathlib.Tactic.Linarith.sub_neg_of_lt one_div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_nonneg IsOrderedRing.toPosMulMono le_of_lt
seminormFromBounded_bddAbove_range 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	BddAbove Set.range DivInvMonoid.toDiv Real.instDivInvMonoid	—	LE.le.eq_or_lt' div_zero seminormFromBounded_aux div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_eq_zero_iff 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	seminormFromBounded_ge LE.le.antisymm MulZeroClass.mul_zero seminormFromBounded_le seminormFromBounded_nonneg
seminormFromBounded_ge 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing seminormFromBounded'	—	LE.le.antisymm MulZeroClass.mul_zero mul_one MulZeroClass.zero_mul le_refl mul_comm div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' le_ciSup seminormFromBounded_bddAbove_range
seminormFromBounded_isNonarchimedean 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul IsNonarchimedean Real.linearOrder Distrib.toAdd	seminormFromBounded'	—	ciSup_le AddTorsor.nonempty le_max_iff div_zero div_le_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' add_mul Distrib.rightDistribClass le_ciSup_of_le seminormFromBounded_bddAbove_range
seminormFromBounded_is_norm_iff 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero Pi.hasLe Real.instLE Pi.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real.instMul Distrib.toAdd Real.instAdd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	Set.preimage Set Set.instSingletonSet	—	seminormFromBounded_ker Set.ext seminormFromBounded_zero Set.mem_singleton_iff Set.mem_preimage seminormFromBounded_eq_zero_iff
seminormFromBounded_ker 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	Set.preimage seminormFromBounded' Set Set.instSingletonSet	—	Set.ext seminormFromBounded_eq_zero_iff
seminormFromBounded_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	ciSup_le AddTorsor.nonempty LE.le.eq_or_lt' div_zero seminormFromBounded_aux div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_mul 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	ciSup_le AddTorsor.nonempty mul_comm mul_assoc map_mul_zero_of_map_zero seminormFromBounded_eq_zero_iff zero_div mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing seminormFromBounded_nonneg div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' le_ciSup_of_le seminormFromBounded_bddAbove_range div_mul_eq_mul_div div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono div_le_div_iff_of_pos_right le_refl
seminormFromBounded_neg 📖	mathematical	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	seminormFromBounded'	—	neg_mul
seminormFromBounded_nonneg 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	le_csSup_of_le seminormFromBounded_bddAbove_range div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing
seminormFromBounded_nonzero 📖	—	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	—	—	Function.ne_iff Pi.zero_apply seminormFromBounded_eq_zero_iff
seminormFromBounded_of_mul_apply 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	le_antisymm ciSup_le AddTorsor.nonempty div_zero MulZeroClass.mul_zero div_self mul_one le_refl map_one_ne_zero le_ciSup zero_div MulZeroClass.zero_mul ciSup_const
seminormFromBounded_of_mul_is_mul 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded'	—	seminormFromBounded_of_mul_apply mul_assoc mul_div_assoc Real.mul_iSup_of_nonneg
seminormFromBounded_of_mul_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	seminormFromBounded'	—	le_antisymm ciSup_le AddTorsor.nonempty div_zero div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing lt_of_le_of_ne' mul_one div_self mul_div_assoc zero_div LE.le.antisymm le_mul_iff_one_le_right IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono lt_of_le_of_ne div_one le_ciSup
seminormFromBounded_one 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	—	one_mul le_antisymm ciSup_le AddTorsor.nonempty div_zero zero_le_one Real.instZeroLEOneClass div_self le_refl map_one_ne_zero le_ciSup
seminormFromBounded_one_le 📖	mathematical	Pi.hasLe Real Real.instLE Pi.instZero Real.instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real.instMul	seminormFromBounded' AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real.instOne	—	le_of_eq seminormFromBounded_one one_mul ciSup_le AddTorsor.nonempty div_zero Real.instZeroLEOneClass
seminormFromBounded_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Real Real.instZero	seminormFromBounded'	—	MulZeroClass.zero_mul zero_div ciSup_const AddTorsor.nonempty

---

← Back to Index