Commit 2023-04-10 18:54 ae633458

View on Github →

feat: port Topology.MetricSpace.PiNat (#3344)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/MetricSpace/Basic.lean

deleted theorem IsComplete.nonempty_interᵢ_of_nonempty_bInter

added theorem IsComplete.nonempty_interᵢ_of_nonempty_binterᵢ

deleted theorem Metric.nonempty_interᵢ_of_nonempty_bInter

added theorem Metric.nonempty_interᵢ_of_nonempty_binterᵢ

Created Mathlib/Topology/MetricSpace/PiNat.lean

added theorem PiCountable.dist_eq_tsum

added theorem PiCountable.dist_le_dist_pi_of_dist_lt

added theorem PiCountable.dist_summable

added theorem PiCountable.min_dist_le_dist_pi

added theorem PiNat.apply_eq_of_dist_lt

added theorem PiNat.apply_eq_of_lt_firstDiff

added theorem PiNat.apply_firstDiff_ne

added def PiNat.cylinder

added theorem PiNat.cylinder_anti

added theorem PiNat.cylinder_eq_cylinder_of_le_firstDiff

added theorem PiNat.cylinder_eq_pi

added theorem PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff

added theorem PiNat.cylinder_zero

added theorem PiNat.disjoint_cylinder_of_longestPrefix_lt

added theorem PiNat.dist_eq_of_ne

added theorem PiNat.dist_triangle_nonarch

added theorem PiNat.exists_disjoint_cylinder

added theorem PiNat.exists_lipschitz_retraction_of_isClosed

added theorem PiNat.exists_retraction_of_isClosed

added theorem PiNat.exists_retraction_subtype_of_isClosed

added theorem PiNat.firstDiff_comm

added theorem PiNat.firstDiff_le_longestPrefix

added theorem PiNat.firstDiff_lt_shortestPrefixDiff

added theorem PiNat.inter_cylinder_longestPrefix_nonempty

added theorem PiNat.isOpen_iff_dist

added theorem PiNat.isTopologicalBasis_cylinders

added theorem PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder

added def PiNat.longestPrefix

added theorem PiNat.mem_cylinder_comm

added theorem PiNat.mem_cylinder_firstDiff

added theorem PiNat.mem_cylinder_iff

added theorem PiNat.mem_cylinder_iff_dist_le

added theorem PiNat.mem_cylinder_iff_eq

added theorem PiNat.mem_cylinder_iff_le_firstDiff

added def PiNat.metricSpaceNatNat

added theorem PiNat.min_firstDiff_le

added theorem PiNat.self_mem_cylinder

added def PiNat.shortestPrefixDiff

added theorem PiNat.shortestPrefixDiff_pos

added theorem PiNat.unionᵢ_cylinder_update

added theorem PiNat.update_mem_cylinder

added theorem exists_nat_nat_continuous_surjective_of_completeSpace