Commit 2023-03-03 08:09 0782bc73

View on Github →

feat: port Topology.MetricSpace.EMetricSpace (#2407)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/EMetricSpace.lean

added def EMetric.ball

added theorem EMetric.ball_disjoint

added theorem EMetric.ball_eq_empty_iff

added theorem EMetric.ball_mem_nhds

added theorem EMetric.ball_prod_same

added theorem EMetric.ball_subset

added theorem EMetric.ball_subset_ball

added theorem EMetric.ball_subset_closedBall

added theorem EMetric.ball_zero

added theorem EMetric.cauchySeq_iff'

added theorem EMetric.cauchySeq_iff

added theorem EMetric.cauchySeq_iff_NNReal

added def EMetric.closedBall

added theorem EMetric.closedBall_mem_nhds

added theorem EMetric.closedBall_prod_same

added theorem EMetric.closedBall_subset_closedBall

added theorem EMetric.closedBall_top

added theorem EMetric.complete_of_cauchySeq_tendsto

added theorem EMetric.complete_of_convergent_controlled_sequences

added theorem EMetric.controlled_of_uniformEmbedding

added theorem EMetric.countable_closure_of_compact

added theorem EMetric.diam_ball

added theorem EMetric.diam_closedBall

added theorem EMetric.diam_empty

added theorem EMetric.diam_eq_supₛ

added theorem EMetric.diam_eq_zero_iff

added theorem EMetric.diam_image_le_iff

added theorem EMetric.diam_insert

added theorem EMetric.diam_le

added theorem EMetric.diam_le_iff

added theorem EMetric.diam_mono

added theorem EMetric.diam_pair

added theorem EMetric.diam_pi_le_of_le

added theorem EMetric.diam_pos_iff'

added theorem EMetric.diam_pos_iff

added theorem EMetric.diam_singleton

added theorem EMetric.diam_subsingleton

added theorem EMetric.diam_triple

added theorem EMetric.diam_union'

added theorem EMetric.diam_union

added theorem EMetric.diam_unionᵢ_mem_option

added def EMetric.edistLtTopSetoid

added theorem EMetric.edist_le_diam_of_mem

added theorem EMetric.edist_le_of_diam_le

added theorem EMetric.exists_ball_subset_ball

added theorem EMetric.inseparable_iff

added theorem EMetric.isClosed_ball_top

added theorem EMetric.isOpen_ball

added theorem EMetric.isOpen_iff

added theorem EMetric.mem_ball'

added theorem EMetric.mem_ball

added theorem EMetric.mem_ball_comm

added theorem EMetric.mem_ball_self

added theorem EMetric.mem_closedBall'

added theorem EMetric.mem_closedBall

added theorem EMetric.mem_closedBall_comm

added theorem EMetric.mem_closedBall_self

added theorem EMetric.mem_closure_iff

added theorem EMetric.mem_nhdsWithin_iff

added theorem EMetric.mem_nhds_iff

added theorem EMetric.nhdsWithin_basis_closed_eball

added theorem EMetric.nhdsWithin_basis_eball

added theorem EMetric.nhds_basis_closed_eball

added theorem EMetric.nhds_basis_eball

added theorem EMetric.nhds_eq

added theorem EMetric.ordConnected_setOf_ball_subset

added theorem EMetric.ordConnected_setOf_closedBall_subset

added theorem EMetric.pos_of_mem_ball

added theorem EMetric.secondCountable_of_almost_dense_set

added theorem EMetric.secondCountable_of_sigmaCompact

added theorem EMetric.subset_countable_closure_of_almost_dense_set

added theorem EMetric.subset_countable_closure_of_compact

added theorem EMetric.tendstoLocallyUniformlyOn_iff

added theorem EMetric.tendstoLocallyUniformly_iff

added theorem EMetric.tendstoUniformlyOn_iff

added theorem EMetric.tendstoUniformly_iff

added theorem EMetric.tendsto_atTop

added theorem EMetric.tendsto_nhds

added theorem EMetric.tendsto_nhdsWithin_nhds

added theorem EMetric.tendsto_nhdsWithin_nhdsWithin

added theorem EMetric.tendsto_nhds_nhds

added theorem EMetric.totallyBounded_iff'

added theorem EMetric.totallyBounded_iff

added theorem EMetric.uniformContinuousOn_iff

added theorem EMetric.uniformContinuous_iff

added theorem EMetric.uniformEmbedding_iff'

added theorem EMetric.uniformInducing_iff

added def EMetricSpace.induced

added def EMetricSpace.ofT0PseudoEMetricSpace

added def EMetricSpace.replaceUniformity

added theorem MulOpposite.edist_op

added theorem MulOpposite.edist_unop

added theorem Prod.edist_eq

added def PseudoEMetricSpace.induced

added def PseudoEMetricSpace.replaceUniformity

added theorem Subtype.edist_eq

added theorem ULift.edist_eq

added theorem ULift.edist_up_up

added theorem UniformSpace.SeparationQuotient.edist_mk

added theorem edist_congr_left

added theorem edist_congr_right

added theorem edist_eq_zero

added theorem edist_le_Ico_sum_edist

added theorem edist_le_Ico_sum_of_edist_le

added theorem edist_le_pi_edist

added theorem edist_le_range_sum_edist

added theorem edist_le_range_sum_of_edist_le

added theorem edist_le_zero

added theorem edist_mem_uniformity

added theorem edist_ofAdd

added theorem edist_ofDual

added theorem edist_ofMul

added theorem edist_pi_const

added theorem edist_pi_const_le

added theorem edist_pi_def

added theorem edist_pi_le_iff

added theorem edist_pos

added theorem edist_toAdd

added theorem edist_toDual

added theorem edist_toMul

added theorem edist_triangle4

added theorem edist_triangle_left

added theorem edist_triangle_right

added theorem eq_of_forall_edist_le

added theorem mem_uniformity_edist

added def uniformSpaceOfEDist

added theorem uniformSpace_edist

added theorem uniformity_basis_edist'

added theorem uniformity_basis_edist

added theorem uniformity_basis_edist_inv_nat

added theorem uniformity_basis_edist_inv_two_pow

added theorem uniformity_basis_edist_le'

added theorem uniformity_basis_edist_le

added theorem uniformity_basis_edist_nnreal

added theorem uniformity_basis_edist_nnreal_le

added theorem uniformity_dist_of_mem_uniformity

added theorem uniformity_edist

added theorem uniformity_pseudoedist

added theorem zero_eq_edist