Ultra

📁 Source: Mathlib/Analysis/Normed/Field/Ultra.lean

Statistics

Metric	Count
Definitions	0
Theorems isUltrametricDist_of_forall_norm_add_one_le_max_norm_one, isUltrametricDist_of_forall_norm_add_one_of_norm_le_one, isUltrametricDist_of_forall_norm_natCast_le_one, isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one, isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm, isUltrametricDist_iff_forall_norm_natCast_le_one	6
Total	6

IsUltrametricDist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUltrametricDist_of_forall_norm_add_one_le_max_norm_one 📖	mathematical	Real Real.instLE Norm.norm NormedDivisionRing.toNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instMax Real.instOne	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	isUltrametricDist_of_forall_norm_add_le_max_norm eq_or_ne add_zero le_max_left norm_pos_iff div_add_one norm_div div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing max_mul_of_nonneg IsOrderedRing.toMulPosMono Real.instIsOrderedRing LT.lt.le div_mul_cancel₀ LT.lt.ne' one_mul
isUltrametricDist_of_forall_norm_add_one_of_norm_le_one 📖	mathematical	Real Real.instLE Norm.norm NormedDivisionRing.toNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instOne	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	isUltrametricDist_of_forall_norm_add_one_le_max_norm_one le_or_gt LE.le.trans le_max_right div_le_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_div add_div div_self LT.lt.trans' zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero add_comm one_div norm_inv LT.lt.le le_max_left
isUltrametricDist_of_forall_norm_natCast_le_one 📖	mathematical	Real Real.instLE Norm.norm NormedDivisionRing.toNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedDivisionRing.toNormedRing Real.instOne	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm nsmul_eq_mul norm_mul NormedDivisionRing.toNormMulClass LE.le.eq_or_lt norm_nonneg MulZeroClass.mul_zero mul_le_iff_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing NormedDivisionRing.to_normOneClass Commute.add_pow Commute.one_right Finset.sum_congr one_pow mul_one Nat.cast_comm LE.le.trans norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Finset.card_range Finset.sum_const max_cases eq_or_ne zero_add pow_zero pow_le_one₀ IsOrderedRing.toPosMulMono pow_le_one_iff_of_nonneg IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass pow_le_pow_right₀ Mathlib.Tactic.Contrapose.contrapose₁ LT.lt.le Nat.instNoMaxOrder
isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one 📖	mathematical	Real Real.instLE Norm.norm NormedDivisionRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Real.instOne	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	norm_neg isUltrametricDist_of_forall_norm_add_one_of_norm_le_one
isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm 📖	mathematical	Real Real.instLE Monoid.toNatPow Real.instMonoid Norm.norm NormedDivisionRing.toNorm Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing NormedDivisionRing.toNormedRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne AddMonoid.toNatSMul Real.instAddMonoid Real.instMax Real.instOne	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	isUltrametricDist_of_forall_norm_add_one_le_max_norm_one max_comm le_of_forall_gt_imp_ge_of_dense LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing max_lt_iff Nat.cast_one Real.exists_natCast_add_one_lt_pow_of_one_lt one_lt_div lt_max_of_lt_left Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat MonotoneOn.map_max pow_left_monotoneOn IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono Real.instZeroLEOneClass norm_nonneg one_pow le_of_pow_le_pow_left₀ zero_add pow_zero max_self one_smul nsmul_eq_mul lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono pow_pos IsStrictOrderedRing.toZeroLEOneClass div_pow LT.lt.le LT.lt.trans zero_lt_one NeZero.charZero_one IsStrictOrderedRing.toCharZero LE.le.trans

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUltrametricDist_iff_forall_norm_natCast_le_one 📖	mathematical	—	IsUltrametricDist PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedDivisionRing.toNormedRing Real Real.instLE Norm.norm NormedDivisionRing.toNorm AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Real.instOne	—	IsUltrametricDist.norm_natCast_le_one NormedDivisionRing.to_normOneClass IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one

---

← Back to Index