Nat

📁 Source: Mathlib/Topology/Instances/Nat.lean

Statistics

Metric	Count
Definitions instDist, instMetricSpace	2
Theorems closedBall_eq_Icc, dist_cast_real, dist_coe_int, dist_eq, instIsOrderBornology, instNoncompactSpace, instProperSpace, isClosedEmbedding_coe_real, isUniformEmbedding_coe_real, pairwise_one_le_dist, preimage_ball, preimage_closedBall	12
Total	14

Nat

Definitions

Name	Category	Theorems
instDist 📖	CompOp	6 math math: dist_cast_real, dist_eq, PNat.dist_coe, pairwise_one_le_dist, dist_cast_rat, dist_coe_int
instMetricSpace 📖	CompOp	5 math math: closedBall_eq_Icc, preimage_closedBall, instIsOrderBornology, preimage_ball, instProperSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedBall_eq_Icc 📖	mathematical	—	Metric.closedBall MetricSpace.toPseudoMetricSpace instMetricSpace Set.Icc instPreorder ceil Real Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing Real.instSub Real.instNatCast floor Real.instAdd	—	Real.instIsStrictOrderedRing le_or_gt preimage_closedBall Real.closedBall_eq_Icc preimage_Icc add_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid cast_nonneg' Real.instZeroLEOneClass Metric.closedBall_eq_empty Set.Icc_eq_empty_of_lt floor_mono le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing floor_natCast lt_ceil lt_of_not_ge Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_nonpos_of_le
dist_cast_real 📖	mathematical	—	Dist.dist Real PseudoMetricSpace.toDist Real.pseudoMetricSpace Real.instNatCast instDist	—	—
dist_coe_int 📖	mathematical	—	Dist.dist Int.instDist instDist	—	—
dist_eq 📖	mathematical	—	Dist.dist instDist abs Real Real.lattice Real.instAddGroup Real.instSub Real.instNatCast	—	—
instIsOrderBornology 📖	mathematical	—	IsOrderBornology PseudoMetricSpace.toBornology MetricSpace.toPseudoMetricSpace instMetricSpace instPreorder	—	IsOrderBornology.of_isCompactIcc ConditionallyCompleteLinearOrder.toCompactIccSpace OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat Real.instIsStrictOrderedRing closedBall_eq_Icc cast_zero zero_sub zero_add
instNoncompactSpace 📖	mathematical	—	NoncompactSpace instTopologicalSpaceNat	—	noncompactSpace_of_neBot Filter.cocompact_eq_cofinite instDiscreteTopologyNat instInfiniteNat
instProperSpace 📖	mathematical	—	ProperSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	Real.instIsStrictOrderedRing closedBall_eq_Icc Set.Finite.isCompact Set.finite_Icc
isClosedEmbedding_coe_real 📖	mathematical	—	Topology.IsClosedEmbedding Real instTopologicalSpaceNat UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instNatCast	—	Metric.isClosedEmbedding_of_pairwise_le_dist instDiscreteTopologyNat zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing pairwise_one_le_dist
isUniformEmbedding_coe_real 📖	mathematical	—	IsUniformEmbedding Real instUniformSpaceNat PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instNatCast	—	Metric.isUniformEmbedding_bot_of_pairwise_le_dist zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing pairwise_one_le_dist
pairwise_one_le_dist 📖	mathematical	—	Pairwise Real Real.instLE Real.instOne Dist.dist instDist	—	Int.pairwise_one_le_dist Int.instCharZero
preimage_ball 📖	mathematical	—	Set.preimage Real Real.instNatCast Metric.ball Real.pseudoMetricSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	—
preimage_closedBall 📖	mathematical	—	Set.preimage Real Real.instNatCast Metric.closedBall Real.pseudoMetricSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	—

---

← Back to Index