PiNat

📁 Source: Mathlib/Topology/MetricSpace/PiNat.lean

Statistics

Metric	Count
Definitions PiNatEmbed, distDenseSeq, embed, emetricSpace, instPseudoEMetricSpace, instPseudoMetricSpace, metricSpace, ofPiNat, toPiNatEquiv, toPiNatHomeo, dist, edist, emetricSpace, metricSpace, pseudoEMetricSpace, pseudoMetricSpace, cylinder, dist, firstDiff, longestPrefix, metricSpace, metricSpaceNatNat, metricSpaceOfDiscreteUniformity, res, shortestPrefixDiff	25
Theorems of_countable_separating, continuous_distDenseSeq, continuous_distDenseSeq_inv, continuous_toPiNat, dist_def, edist_def, embed_injective, exists_closed_embedding_to_hilbert_cube, exists_embedding_to_hilbert_cube, ext, ext_iff, forall, injective_distDenseSeq, isHomeomorph_toPiNat, isUniformEmbedding_embed, isometry_embed, ofPiNat_inj, separation, toPiNatEquiv_apply_ofPiNat, toPiNatEquiv_symm_apply, toPiNatHomeo_apply_ofPiNat, toPiNatHomeo_symm_apply, dist_eq_tsum, dist_le_dist_pi_of_dist_lt, dist_summable, edist_eq_tsum, edist_le_edist_pi_of_edist_lt, edist_le_two, edist_lt_top, min_dist_le_dist_pi, min_edist_le_edist_pi, apply_eq_of_dist_lt, apply_eq_of_lt_firstDiff, apply_firstDiff_ne, boundedSpace, completeSpace, cylinder_anti, cylinder_eq_cylinder_of_le_firstDiff, cylinder_eq_pi, cylinder_eq_res, cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff, cylinder_zero, disjoint_cylinder_of_longestPrefix_lt, dist_comm, dist_eq_of_ne, dist_le_one, dist_nonneg, dist_self, dist_triangle, dist_triangle_nonarch, eq_of_dist_eq_zero, exists_disjoint_cylinder, exists_lipschitz_retraction_of_isClosed, exists_retraction_of_isClosed, exists_retraction_subtype_of_isClosed, firstDiff_comm, firstDiff_def, firstDiff_le_longestPrefix, firstDiff_lt_shortestPrefixDiff, iUnion_cylinder_update, inter_cylinder_longestPrefix_nonempty, isOpen_cylinder, isOpen_iff_dist, isTopologicalBasis_cylinders, lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder, mem_cylinder_comm, mem_cylinder_firstDiff, mem_cylinder_iff, mem_cylinder_iff_dist_le, mem_cylinder_iff_eq, mem_cylinder_iff_le_firstDiff, min_firstDiff_le, res_eq_res, res_injective, res_length, res_succ, res_zero, self_mem_cylinder, shortestPrefixDiff_pos, update_mem_cylinder, exists_nat_nat_continuous_surjective_of_completeSpace	81
Total	106

Metric

Definitions

Name	Category	Theorems
PiNatEmbed 📖	CompData	12 math math: PiNatEmbed.continuous_distDenseSeq_inv, PiNatEmbed.toPiNatEquiv_apply_ofPiNat, PiNatEmbed.edist_def, PiNatEmbed.continuous_toPiNat, PiNatEmbed.dist_def, PiNatEmbed.isHomeomorph_toPiNat, PiNatEmbed.embed_injective, PiNatEmbed.toPiNatHomeo_apply_ofPiNat, PiNatEmbed.toPiNatHomeo_symm_apply, PiNatEmbed.isUniformEmbedding_embed, PiNatEmbed.toPiNatEquiv_symm_apply, PiNatEmbed.isometry_embed

Metric.PiNatEmbed

Definitions

Name	Category	Theorems
distDenseSeq 📖	CompOp	3 math math: continuous_distDenseSeq_inv, separation, continuous_distDenseSeq
embed 📖	CompOp	3 math math: embed_injective, isUniformEmbedding_embed, isometry_embed
emetricSpace 📖	CompOp	—
instPseudoEMetricSpace 📖	CompOp	3 math math: edist_def, isUniformEmbedding_embed, isometry_embed
instPseudoMetricSpace 📖	CompOp	6 math math: continuous_distDenseSeq_inv, continuous_toPiNat, dist_def, isHomeomorph_toPiNat, toPiNatHomeo_apply_ofPiNat, toPiNatHomeo_symm_apply
metricSpace 📖	CompOp	—
ofPiNat 📖	CompOp	9 math math: continuous_distDenseSeq_inv, ofPiNat_inj, toPiNatEquiv_apply_ofPiNat, edist_def, dist_def, ext_iff, toPiNatHomeo_apply_ofPiNat, toPiNatHomeo_symm_apply, toPiNatEquiv_symm_apply
toPiNatEquiv 📖	CompOp	2 math math: toPiNatEquiv_apply_ofPiNat, toPiNatEquiv_symm_apply
toPiNatHomeo 📖	CompOp	2 math math: toPiNatHomeo_apply_ofPiNat, toPiNatHomeo_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_distDenseSeq 📖	mathematical	—	Continuous Set.Elem Real unitInterval UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instTopologicalSpaceSubtype Set Set.instMembership Real.pseudoMetricSpace distDenseSeq	—	isEmpty_or_nonempty continuous_of_discreteTopology Finite.instDiscreteTopology T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Finite.of_subsingleton IsEmpty.instSubsingleton Continuous.comp continuous_projIcc instOrderTopologyReal Continuous.dist continuous_id' continuous_const
continuous_distDenseSeq_inv 📖	mathematical	—	Continuous Metric.PiNatEmbed Set.Elem Real unitInterval distDenseSeq UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpace Nat.encodable Subtype.pseudoMetricSpace Real.pseudoMetricSpace Set Set.instMembership MetricSpace.toPseudoMetricSpace ofPiNat	—	continuous_iff_continuousAt separation Topology.IsInducing.nhds_eq_comap Topology.IsEmbedding.toIsInducing IsUniformEmbedding.isEmbedding isUniformEmbedding_embed injective_distDenseSeq nhds_pi Filter.mem_pi_of_mem
continuous_toPiNat 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	Metric.PiNatEmbed instPseudoMetricSpace toPiNat	—	continuous_iff_continuous_dist continuous_tsum Real.instCompleteSpace Nat.instAtLeastTwoHAddOfNat Continuous.min OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_const Continuous.dist Continuous.comp' Continuous.fst continuous_id' Continuous.snd summable_geometric_two_encode inv_pow abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing one_div
dist_def 📖	mathematical	—	Dist.dist Metric.PiNatEmbed PseudoMetricSpace.toDist instPseudoMetricSpace tsum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMin Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Encodable.encode ofPiNat SummationFilter.unconditional	—	—
edist_def 📖	mathematical	—	EDist.edist Metric.PiNatEmbed PseudoEMetricSpace.toEDist instPseudoEMetricSpace tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace ENNReal.instMin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Encodable.encode ofPiNat SummationFilter.unconditional	—	—
embed_injective 📖	mathematical	Pairwise	Metric.PiNatEmbed embed	—	not_imp_comm
exists_closed_embedding_to_hilbert_cube 📖	mathematical	—	Topology.IsEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership Real.pseudoMetricSpace	—	exists_embedding_to_hilbert_cube
exists_embedding_to_hilbert_cube 📖	mathematical	—	Topology.IsEmbedding UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership Real.pseudoMetricSpace	—	continuous_toPiNat continuous_distDenseSeq continuous_distDenseSeq_inv IsUniformEmbedding.isEmbedding isUniformEmbedding_embed injective_distDenseSeq Topology.IsEmbedding.comp Homeomorph.isEmbedding
ext 📖	—	ofPiNat	—	—	—
ext_iff 📖	mathematical	—	ofPiNat	—	ext
forall 📖	mathematical	—	toPiNat	—	Equiv.forall_congr_left
injective_distDenseSeq 📖	—	—	—	—	separation IsOpen.mem_nhds isOpen_compl_singleton T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
isHomeomorph_toPiNat 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pairwise	IsHomeomorph Metric.PiNatEmbed instPseudoMetricSpace toPiNat	—	isHomeomorph_iff_continuous_bijective TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace continuous_toPiNat Equiv.bijective
isUniformEmbedding_embed 📖	mathematical	Pairwise	IsUniformEmbedding Metric.PiNatEmbed PseudoEMetricSpace.toUniformSpace instPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace Pi.uniformSpace embed	—	Isometry.isUniformEmbedding isometry_embed
isometry_embed 📖	mathematical	—	Isometry Metric.PiNatEmbed instPseudoEMetricSpace PiCountable.pseudoEMetricSpace embed	—	PseudoEMetricSpace.isometry_induced
ofPiNat_inj 📖	mathematical	—	ofPiNat	—	Equiv.injective
separation 📖	mathematical	Set Filter Filter.instMembership nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	Filter.comap Set.Elem Real unitInterval distDenseSeq instTopologicalSpaceSubtype Set.instMembership Real.pseudoMetricSpace	—	Set.eq_empty_or_nonempty closure_compl Nat.instAtLeastTwoHAddOfNat Metric.denseRange_iff TopologicalSpace.denseRange_denseSeq PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass NeZero.one Real.instNontrivial Real.instIsOrderedRing IsOpen.mem_nhds Metric.isOpen_ball sup_of_le_right dist_zero_right abs_eq_self Real.instIsOrderedAddMonoid MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono one_mul IsOrderedAddMonoid.toAddLeftMono IsStrictOrderedRing.toCharZero LT.lt.trans_le LE.le.trans_lt dist_triangle_right add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_halves CharZero.NeZero.two notMem_of_notMem_closure Metric.infDist_le_dist_of_mem LT.lt.not_ge
toPiNatEquiv_apply_ofPiNat 📖	mathematical	—	ofPiNat DFunLike.coe Equiv Metric.PiNatEmbed EquivLike.toFunLike Equiv.instEquivLike toPiNatEquiv	—	—
toPiNatEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Metric.PiNatEmbed EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toPiNatEquiv ofPiNat	—	—
toPiNatHomeo_apply_ofPiNat 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pairwise	ofPiNat DFunLike.coe Homeomorph Metric.PiNatEmbed instPseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike toPiNatHomeo	—	—
toPiNatHomeo_symm_apply 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pairwise	DFunLike.coe Homeomorph Metric.PiNatEmbed instPseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm toPiNatHomeo ofPiNat	—	—

Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_countable_separating 📖	mathematical	Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Pairwise	TopologicalSpace.MetrizableSpace	—	Topology.IsEmbedding.metrizableSpace EMetricSpace.metrizableSpace Homeomorph.isEmbedding

PiCountable

Definitions

Name	Category	Theorems
dist 📖	CompOp	2 math math: min_dist_le_dist_pi, dist_eq_tsum
edist 📖	CompOp	4 math math: min_edist_le_edist_pi, edist_eq_tsum, edist_le_two, edist_lt_top
emetricSpace 📖	CompOp	—
metricSpace 📖	CompOp	—
pseudoEMetricSpace 📖	CompOp	1 math math: Metric.PiNatEmbed.isometry_embed
pseudoMetricSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq_tsum 📖	mathematical	—	Dist.dist dist tsum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMin Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Encodable.encode PseudoMetricSpace.toDist SummationFilter.unconditional	—	—
dist_le_dist_pi_of_dist_lt 📖	mathematical	Real Real.instLT Dist.dist dist Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Encodable.encode	Real.instLE PseudoMetricSpace.toDist	—	Nat.instAtLeastTwoHAddOfNat not_le min_le_iff min_dist_le_dist_pi
dist_summable 📖	mathematical	—	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMin Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Encodable.encode Dist.dist PseudoMetricSpace.toDist SummationFilter.unconditional	—	Summable.of_nonneg_of_le Nat.instAtLeastTwoHAddOfNat le_min le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo dist_nonneg min_le_left inv_pow one_div summable_geometric_two_encode
edist_eq_tsum 📖	mathematical	—	EDist.edist edist tsum ENNReal ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace ENNReal.instMin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Encodable.encode SummationFilter.unconditional	—	—
edist_le_edist_pi_of_edist_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist edist Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Encodable.encode	Preorder.toLE	—	Nat.instAtLeastTwoHAddOfNat not_le min_le_iff min_edist_le_edist_pi
edist_le_two 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist edist instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat	—	LE.le.trans' Nat.instAtLeastTwoHAddOfNat ENNReal.tsum_geometric_two_encode_le_two edist_eq_tsum Summable.tsum_le_tsum ENNReal.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional min_le_left ENNReal.summable
edist_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist edist Top.top instTopENNReal	—	LE.le.trans_lt Nat.instAtLeastTwoHAddOfNat edist_le_two
min_dist_le_dist_pi 📖	mathematical	—	Real Real.instLE Real.instMin Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Encodable.encode Dist.dist PseudoMetricSpace.toDist dist	—	Summable.le_tsum Real.instIsOrderedAddMonoid OrderTopology.to_orderClosedTopology instOrderTopologyReal Nat.instAtLeastTwoHAddOfNat SummationFilter.instNeBotUnconditional SummationFilter.instLeAtTopUnconditional dist_summable le_min inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing dist_nonneg
min_edist_le_edist_pi 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instMin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Nat.instAtLeastTwoHAddOfNat Encodable.encode EDist.edist edist	—	ENNReal.le_tsum

PiNat

Definitions

Name	Category	Theorems
cylinder 📖	CompOp	20 math math: cylinder_eq_cylinder_of_le_firstDiff, update_mem_cylinder, cylinder_eq_res, isTopologicalBasis_cylinders, iUnion_cylinder_update, cylinder_zero, mem_cylinder_iff_dist_le, inter_cylinder_longestPrefix_nonempty, isOpen_cylinder, cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff, cylinder_eq_pi, mem_cylinder_firstDiff, mem_cylinder_iff_le_firstDiff, self_mem_cylinder, mem_cylinder_comm, mem_cylinder_iff_eq, mem_cylinder_iff, disjoint_cylinder_of_longestPrefix_lt, cylinder_anti, exists_disjoint_cylinder
dist 📖	CompOp	9 math math: dist_triangle_nonarch, dist_triangle, lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder, mem_cylinder_iff_dist_le, dist_eq_of_ne, dist_nonneg, dist_self, dist_le_one, dist_comm
firstDiff 📖	CompOp	8 math math: firstDiff_def, firstDiff_le_longestPrefix, dist_eq_of_ne, firstDiff_comm, mem_cylinder_firstDiff, firstDiff_lt_shortestPrefixDiff, mem_cylinder_iff_le_firstDiff, min_firstDiff_le
longestPrefix 📖	CompOp	2 math math: inter_cylinder_longestPrefix_nonempty, firstDiff_le_longestPrefix
metricSpace 📖	CompOp	3 math math: boundedSpace, exists_lipschitz_retraction_of_isClosed, completeSpace
metricSpaceNatNat 📖	CompOp	—
metricSpaceOfDiscreteUniformity 📖	CompOp	—
res 📖	CompOp	7 math math: cylinder_eq_res, res_zero, CantorScheme.map_mem, res_injective, res_length, res_succ, res_eq_res
shortestPrefixDiff 📖	CompOp	2 math math: firstDiff_lt_shortestPrefixDiff, shortestPrefixDiff_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_of_dist_lt 📖	—	Real Real.instLT Dist.dist dist Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne dist_eq_of_ne one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero apply_eq_of_lt_firstDiff LE.le.trans_lt
apply_eq_of_lt_firstDiff 📖	—	firstDiff	—	—	Nat.find_min Function.ne_iff firstDiff_def not_lt_zero'
apply_firstDiff_ne 📖	—	—	—	—	firstDiff_def Nat.find_spec Function.ne_iff
boundedSpace 📖	mathematical	DiscreteTopology	BoundedSpace PseudoMetricSpace.toBornology MetricSpace.toPseudoMetricSpace metricSpace	—	Metric.boundedSpace_iff dist_le_one
completeSpace 📖	mathematical	DiscreteTopology	CompleteSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace metricSpace	—	Metric.complete_of_convergent_controlled_sequences Nat.instAtLeastTwoHAddOfNat one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial tendsto_pi_nhds Filter.Tendsto.congr' Filter.mp_mem Filter.Ici_mem_atTop Filter.univ_mem' apply_eq_of_dist_lt le_rfl tendsto_const_nhds
cylinder_anti 📖	mathematical	—	Set Set.instHasSubset cylinder	—	LT.lt.trans_le
cylinder_eq_cylinder_of_le_firstDiff 📖	mathematical	firstDiff	cylinder	—	mem_cylinder_iff_eq apply_eq_of_lt_firstDiff LT.lt.trans_le
cylinder_eq_pi 📖	mathematical	—	cylinder Set.pi SetLike.coe Finset Finset.instSetLike Finset.range Set Set.instSingletonSet	—	Set.ext Finset.coe_range
cylinder_eq_res 📖	mathematical	—	cylinder setOf res	—	Set.ext res_eq_res
cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff 📖	mathematical	DiscreteTopology Set.Nonempty longestPrefix firstDiff Set Set.instMembership	cylinder	—	lt_trichotomy inter_cylinder_longestPrefix_nonempty disjoint_cylinder_of_longestPrefix_lt Set.Nonempty.not_disjoint cylinder_eq_cylinder_of_le_firstDiff LT.lt.le firstDiff_comm Set.Nonempty.mono Set.inter_subset_inter_right cylinder_anti mem_cylinder_iff_eq mem_cylinder_firstDiff
cylinder_zero 📖	mathematical	—	cylinder Set.univ	—	cylinder_eq_pi Finset.coe_empty Set.empty_pi
disjoint_cylinder_of_longestPrefix_lt 📖	mathematical	DiscreteTopology Set Set.instMembership longestPrefix	Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice cylinder	—	Mathlib.Tactic.Contrapose.contrapose₁ Set.not_disjoint_iff_nonempty_inter le_trans mem_cylinder_iff_le_firstDiff mem_cylinder_comm firstDiff_le_longestPrefix
dist_comm 📖	mathematical	—	Dist.dist dist	—	one_div inv_pow firstDiff_comm
dist_eq_of_ne 📖	mathematical	—	Dist.dist dist Real Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat firstDiff	—	Nat.instAtLeastTwoHAddOfNat one_div inv_pow
dist_le_one 📖	mathematical	—	Real Real.instLE Dist.dist dist Real.instOne	—	eq_or_ne Real.instZeroLEOneClass one_div inv_pow inv_le_one_of_one_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_le_pow₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_le_true Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo
dist_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero Dist.dist dist	—	eq_or_ne one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing
dist_self 📖	mathematical	—	Dist.dist dist Real Real.instZero	—	—
dist_triangle 📖	mathematical	—	Real Real.instLE Dist.dist dist Real.instAdd	—	dist_triangle_nonarch max_le_add_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add dist_nonneg
dist_triangle_nonarch 📖	mathematical	—	Real Real.instLE Dist.dist dist Real.instMax	—	eq_or_ne dist_self Nat.instAtLeastTwoHAddOfNat dist_eq_of_ne one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass NeZero.one Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd min_le_iff min_firstDiff_le
eq_of_dist_eq_zero 📖	—	Dist.dist dist Real Real.instZero	—	—	eq_or_ne Nat.instAtLeastTwoHAddOfNat dist_eq_of_ne one_div inv_pow isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Real.instIsStrictOrderedRing AddGroup.existsAddOfLE Real.instNontrivial IsStrictOrderedRing.toCharZero
exists_disjoint_cylinder 📖	mathematical	DiscreteTopology Set Set.instMembership	Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice cylinder	—	Set.eq_empty_or_nonempty cylinder_zero IsClosed.notMem_iff_infDist_pos Nat.instAtLeastTwoHAddOfNat exists_pow_lt_of_lt_one Real.instIsStrictOrderedRing Real.instArchimedean AddGroup.existsAddOfLE one_half_lt_one PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Set.disjoint_left lt_irrefl Metric.infDist_le_dist_of_mem mem_cylinder_iff_dist_le mem_cylinder_comm
exists_lipschitz_retraction_of_isClosed 📖	mathematical	DiscreteTopology Set.Nonempty	Set.range LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace metricSpace NNReal instOneNNReal	—	inter_cylinder_longestPrefix_nonempty Set.Subset.antisymm Set.mem_range_self LipschitzWith.mk_one eq_or_ne dist_self mem_cylinder_iff_eq mem_cylinder_firstDiff le_refl firstDiff_comm cylinder_anti firstDiff_le_longestPrefix Set.Nonempty.some_mem mem_cylinder_iff_le_firstDiff cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff Nat.instAtLeastTwoHAddOfNat dist_eq_of_ne one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero
exists_retraction_of_isClosed 📖	mathematical	DiscreteTopology Set.Nonempty	Set.range Continuous Pi.topologicalSpace	—	exists_lipschitz_retraction_of_isClosed LipschitzWith.continuous
exists_retraction_subtype_of_isClosed 📖	mathematical	DiscreteTopology Set.Nonempty	Set Set.instMembership Set.Elem Continuous Pi.topologicalSpace instTopologicalSpaceSubtype	—	exists_retraction_of_isClosed Set.mem_range_self
firstDiff_comm 📖	mathematical	—	firstDiff	—	firstDiff_def Nat.find.congr_simp
firstDiff_def 📖	mathematical	—	firstDiff Nat.find	—	—
firstDiff_le_longestPrefix 📖	mathematical	DiscreteTopology Set Set.instMembership	firstDiff longestPrefix	—	longestPrefix.eq_1 le_tsub_iff_right CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le shortestPrefixDiff_pos firstDiff_lt_shortestPrefixDiff
firstDiff_lt_shortestPrefixDiff 📖	mathematical	DiscreteTopology Set Set.instMembership	firstDiff shortestPrefixDiff	—	exists_disjoint_cylinder shortestPrefixDiff.eq_1 Nat.find_spec Mathlib.Tactic.Contrapose.contrapose₁ Set.not_disjoint_iff_nonempty_inter mem_cylinder_comm cylinder_anti mem_cylinder_firstDiff
iUnion_cylinder_update 📖	mathematical	—	Set.iUnion cylinder Function.update	—	Set.ext Function.update_of_ne LT.lt.ne Function.update_self
inter_cylinder_longestPrefix_nonempty 📖	mathematical	DiscreteTopology Set.Nonempty	Set Set.instInter cylinder longestPrefix	—	self_mem_cylinder exists_disjoint_cylinder LT.lt.ne' shortestPrefixDiff_pos longestPrefix.eq_1 shortestPrefixDiff.eq_1 Nat.find_min mem_cylinder_iff_eq
isOpen_cylinder 📖	mathematical	DiscreteTopology	IsOpen Pi.topologicalSpace cylinder	—	cylinder_eq_pi isOpen_set_pi Finset.finite_toSet isOpen_discrete
isOpen_iff_dist 📖	mathematical	DiscreteTopology	IsOpen Pi.topologicalSpace Real Real.instLT Real.instZero Set Set.instMembership	—	TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isTopologicalBasis_cylinders Nat.instAtLeastTwoHAddOfNat one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial mem_cylinder_iff_eq apply_eq_of_dist_lt LT.lt.le TopologicalSpace.IsTopologicalBasis.isOpen_iff exists_pow_lt_of_lt_one Real.instArchimedean AddGroup.existsAddOfLE one_half_lt_one self_mem_cylinder dist_comm LE.le.trans_lt mem_cylinder_iff_dist_le
isTopologicalBasis_cylinders 📖	mathematical	DiscreteTopology	TopologicalSpace.IsTopologicalBasis Pi.topologicalSpace setOf Set cylinder	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_cylinder TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open isTopologicalBasis_pi TopologicalSpace.isTopologicalBasis_opens Finset.bddAbove self_mem_cylinder Set.Subset.trans mem_cylinder_iff LE.le.trans_lt lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist dist Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat LE.le.trans dist_comm mem_cylinder_iff_dist_le eq_or_ne dist_self dist_eq_of_ne firstDiff_comm mem_cylinder_firstDiff
mem_cylinder_comm 📖	mathematical	—	Set Set.instMembership cylinder	—	—
mem_cylinder_firstDiff 📖	mathematical	—	Set Set.instMembership cylinder firstDiff	—	apply_eq_of_lt_firstDiff
mem_cylinder_iff 📖	mathematical	—	Set Set.instMembership cylinder	—	—
mem_cylinder_iff_dist_le 📖	mathematical	—	Set Set.instMembership cylinder Real Real.instLE Dist.dist dist Monoid.toNatPow Real.instMonoid DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne dist_self one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass IsOrderedRing.toPosMulMono Real.instIsOrderedRing apply_firstDiff_ne apply_eq_of_lt_firstDiff LT.lt.trans_le dist_eq_of_ne MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instNontrivial IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toCharZero
mem_cylinder_iff_eq 📖	mathematical	—	Set Set.instMembership cylinder	—	Set.Subset.antisymm self_mem_cylinder
mem_cylinder_iff_le_firstDiff 📖	mathematical	—	Set Set.instMembership cylinder firstDiff	—	apply_firstDiff_ne apply_eq_of_lt_firstDiff LT.lt.trans_le
min_firstDiff_le 📖	mathematical	—	firstDiff	—	apply_firstDiff_ne apply_eq_of_lt_firstDiff lt_min_iff
res_eq_res 📖	mathematical	—	res	—	Nat.instCanonicallyOrderedAdd instIsEmptyFalse LT.lt.trans
res_injective 📖	mathematical	—	res	—	res_eq_res
res_length 📖	mathematical	—	res	—	—
res_succ 📖	mathematical	—	res	—	—
res_zero 📖	mathematical	—	res	—	—
self_mem_cylinder 📖	mathematical	—	Set Set.instMembership cylinder	—	—
shortestPrefixDiff_pos 📖	mathematical	DiscreteTopology Set.Nonempty Set Set.instMembership	shortestPrefixDiff	—	LE.le.trans_lt zero_le Nat.instCanonicallyOrderedAdd firstDiff_lt_shortestPrefixDiff
update_mem_cylinder 📖	mathematical	—	Set Set.instMembership cylinder Function.update	—	mem_cylinder_iff Function.update_of_ne LT.lt.ne

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_nat_continuous_surjective_of_completeSpace 📖	mathematical	—	Continuous Pi.topologicalSpace instTopologicalSpaceNat UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	Nat.instAtLeastTwoHAddOfNat one_div PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo TopologicalSpace.exists_dense_seq TopologicalSpace.SecondCountableTopology.to_separableSpace Set.mem_iInter Set.Nonempty.some_mem continuous_iff_continuousAt continuousAt_of_locally_lipschitz zero_lt_one Real.instZeroLEOneClass NeZero.one eq_or_ne dist_self MulZeroClass.mul_zero Subtype.coe_injective PiNat.apply_firstDiff_ne PiNat.apply_eq_of_dist_lt pow_zero le_rfl PiNat.dist_eq_of_ne PiNat.mem_cylinder_firstDiff LT.lt.ne' dist_triangle_right add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz DenseRange.exists_dist_lt inv_pow LT.lt.le dist_le_zero Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE Real.instArchimedean instOrderTopologyReal ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat add_zero isClosed_iff_clusterPt Filter.Tendsto.const_mul IsTopologicalSemiring.toContinuousMul squeeze_zero Metric.diam_nonneg Metric.diam_closedBall pow_nonneg IsOrderedRing.toPosMulMono Metric.nonempty_iInter_of_nonempty_biInter Metric.isClosed_closedBall Metric.isBounded_closedBall clusterPt_principal_iff Metric.ball_mem_nhds pow_pos Set.iInter_congr Metric.mem_ball' Set.Nonempty.mono Set.iInter_subset_iInter₂ PiNat.exists_retraction_subtype_of_isClosed instDiscreteTopologyNat Function.Surjective.nonempty Continuous.comp

---

← Back to Index