Uniformity

📁 Source: Mathlib/Topology/Metrizable/Uniformity.lean

Statistics

Metric	Count
Definitions ofPreNNDist, metrizableSpaceMetric, pseudoMetrizableSpacePseudoMetric, metricSpace, pseudoMetricSpace	5
Theorems metrizableSpace, pseudoMetrizableSpace, dist_ofPreNNDist, dist_ofPreNNDist_le, le_two_mul_dist_ofPreNNDist, metrizableSpace, metrizable_uniformity	7
Total	12

EMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
metrizableSpace 📖	mathematical	—	TopologicalSpace.MetrizableSpace UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace toPseudoEMetricSpace	—	TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace instT0Space PseudoEMetricSpace.pseudoMetrizableSpace

PseudoEMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pseudoMetrizableSpace 📖	mathematical	—	TopologicalSpace.PseudoMetrizableSpace UniformSpace.toTopologicalSpace toUniformSpace	—	UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity

PseudoMetricSpace

Definitions

Name	Category	Theorems
ofPreNNDist 📖	CompOp	3 math math: le_two_mul_dist_ofPreNNDist, dist_ofPreNNDist, dist_ofPreNNDist_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_ofPreNNDist 📖	mathematical	NNReal instZeroNNReal	Dist.dist toDist ofPreNNDist NNReal.toReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	—
dist_ofPreNNDist_le 📖	mathematical	NNReal instZeroNNReal	Real Real.instLE Dist.dist toDist ofPreNNDist NNReal.toReal	—	NNReal.coe_le_coe LE.le.trans_eq ciInf_le OrderBot.bddBelow add_zero
le_two_mul_dist_ofPreNNDist 📖	mathematical	NNReal instZeroNNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.instAtLeastTwoHAddOfNat NNReal.instMax	Real Real.instLE NNReal.toReal Real.instMul Real.instNatCast Dist.dist toDist ofPreNNDist	—	Nat.instAtLeastTwoHAddOfNat dist_ofPreNNDist NNReal.coe_two NNReal.coe_mul NNReal.mul_iInf NNReal.coe_le_coe le_ciInf nonpos_iff_eq_zero NNReal.instCanonicallyOrderedAdd max_self MulZeroClass.mul_zero Nat.strong_induction_on zero_add min_self eq_or_ne not_lt List.IsChain.rel_cons List.isChain_cons_append_singleton_iff_forall₂ List.forall_zipWith List.forall_iff_forall_mem List.sum_eq_zero_iff IsOrderedRing.toIsOrderedAddMonoid NNReal.instIsOrderedRing add_le_iff_nonpos_left covariant_swap_add_of_covariant_add NNReal.addLeftMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add NNReal.addLeftReflectLT two_mul Set.mem_setOf_eq csSup_le Nat.sSup_mem le_csSup min_eq_left LT.lt.le LE.le.trans Option.coe_def Membership.mem.out List.single_le_sum zero_le LE.le.eq_or_lt le_rfl List.cons_getElem_drop_succ LE.le.not_gt List.sum_take_add_sum_drop add_le_add_iff_right add_le_add_iff_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd le_imp_le_of_le_of_le le_refl mul_le_mul_right NNReal.mulLeftMono max_le

TopologicalSpace

Definitions

Name	Category	Theorems
metrizableSpaceMetric 📖	CompOp	—
pseudoMetrizableSpacePseudoMetric 📖	CompOp	—

UniformSpace

Definitions

Name	Category	Theorems
metricSpace 📖	CompOp	—
pseudoMetricSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
metrizableSpace 📖	mathematical	—	TopologicalSpace.MetrizableSpace toTopologicalSpace	—	TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace pseudoMetrizableSpace
metrizable_uniformity 📖	mathematical	—	PseudoMetricSpace.toUniformSpace	—	has_seq_basis Filter.HasAntitoneBasis.subbasis_with_rel Filter.Tendsto.eventually Filter.HasAntitoneBasis.tendsto_smallSets eventually_uniformity_iterate_comp_subset Filter.HasAntitoneBasis.mem Nat.instAtLeastTwoHAddOfNat Real.instIsStrictOrderedRing Nonneg.coe_inv Nonneg.coe_div Nonneg.coe_zpow one_div inv_pow isReduced_of_noZeroDivisors NNReal.instNoZeroDivisors IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing Filter.HasBasis.inseparable_iff_uniformity Filter.HasAntitoneBasis.toHasBasis SetRel.comm Nat.find.congr_simp half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono one_pos LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one NNReal.half_lt_self one_ne_zero PseudoMetricSpace.dist_ofPreNNDist_le StrictAnti.le_iff_ge pow_right_strictAnti₀ Nat.find_le_iff Filter.HasAntitoneBasis.antitone le_rfl LT.lt.not_ge pow_pos PseudoMetricSpace.le_two_mul_dist_ofPreNNDist Eq.trans_le div_le_iff₀' zero_lt_two NNReal.addLeftMono mul_one_div pow_succ Nat.find_spec lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid zero_le NNReal.instCanonicallyOrderedAdd ext Filter.HasBasis.ext Metric.uniformity_basis_dist_pow NNReal.coe_lt_coe Set.mem_Ioo LE.le.trans_lt NNReal.coe_pow not_le Mathlib.Tactic.Contrapose.contrapose₁ le_trans NNReal.coe_two NNReal.coe_div NNReal.coe_le_coe div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono div_mul_cancel₀ two_ne_zero ZeroLEOneClass.neZero.two IsStrictOrderedRing.toPosMulStrictMono Real.instZeroLEOneClass Real.instIsOrderedAddMonoid Set.mem_setOf_eq

---

← Back to Index