Commit 2023-03-04 08:59 70daecbe

View on Github →

feat: Port Topology.MetricSpace.Infsep (#2613)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Infsep.lean

added theorem Set.Finite.einfsep

added theorem Set.Finite.einfsep_exists_of_nontrivial

added theorem Set.Finite.einfsep_pos

added theorem Set.Finite.infsep

added theorem Set.Finite.infsep_exists_of_nontrivial

added theorem Set.Finite.infsep_of_nontrivial

added theorem Set.Finite.infsep_pos_iff_nontrivial

added theorem Set.Finite.infsep_zero_iff_subsingleton

added theorem Set.Finite.relatively_discrete

added theorem Set.Finset.coe_einfsep

added theorem Set.Finset.coe_infsep

added theorem Set.Finset.coe_infsep_of_offDiag_empty

added theorem Set.Finset.coe_infsep_of_offDiag_nonempty

added theorem Set.Finset.infsep_pos_iff_nontrivial

added theorem Set.Finset.infsep_zero_iff_subsingleton

added theorem Set.Nontrivial.einfsep_exists_of_finite

added theorem Set.Nontrivial.einfsep_lt_top

added theorem Set.Nontrivial.einfsep_ne_top

added theorem Set.Nontrivial.infsep_anti

added theorem Set.Nontrivial.infsep_eq_infᵢ

added theorem Set.Nontrivial.infsep_exists_of_finite

added theorem Set.Nontrivial.infsep_lt_iff

added theorem Set.Nontrivial.infsep_of_fintype

added theorem Set.Nontrivial.le_infsep

added theorem Set.Nontrivial.le_infsep_iff

added theorem Set.Subsingleton.einfsep

added theorem Set.Subsingleton.infsep_zero

added theorem Set.einfsep_anti

added theorem Set.einfsep_empty

added theorem Set.einfsep_eq_infᵢ

added theorem Set.einfsep_eq_top_iff

added theorem Set.einfsep_insert

added theorem Set.einfsep_insert_le

added theorem Set.einfsep_le_edist_of_mem

added theorem Set.einfsep_le_of_mem_of_edist_le

added theorem Set.einfsep_lt_iff

added theorem Set.einfsep_lt_top

added theorem Set.einfsep_lt_top_iff

added theorem Set.einfsep_ne_top

added theorem Set.einfsep_ne_top_iff

added theorem Set.einfsep_of_fintype

added theorem Set.einfsep_pair

added theorem Set.einfsep_pair_eq_inf

added theorem Set.einfsep_pair_le_left

added theorem Set.einfsep_pair_le_right

added theorem Set.einfsep_pos

added theorem Set.einfsep_pos_of_finite

added theorem Set.einfsep_singleton

added theorem Set.einfsep_top

added theorem Set.einfsep_triple

added theorem Set.einfsep_unionᵢ_mem_option

added theorem Set.einfsep_zero

added theorem Set.infsep_empty

added theorem Set.infsep_eq_infᵢ

added theorem Set.infsep_le_dist_of_mem

added theorem Set.infsep_le_of_mem_of_edist_le

added theorem Set.infsep_nonneg

added theorem Set.infsep_of_fintype

added theorem Set.infsep_pair

added theorem Set.infsep_pair_eq_toReal

added theorem Set.infsep_pair_le_toReal_inf

added theorem Set.infsep_pos

added theorem Set.infsep_pos_iff_nontrivial_of_finite

added theorem Set.infsep_singleton

added theorem Set.infsep_triple

added theorem Set.infsep_zero

added theorem Set.infsep_zero_iff_subsingleton_of_finite

added theorem Set.le_edist_of_le_einfsep

added theorem Set.le_edist_of_le_infsep

added theorem Set.le_einfsep

added theorem Set.le_einfsep_iff

added theorem Set.le_einfsep_image_iff

added theorem Set.le_einfsep_of_forall_dist_le

added theorem Set.le_einfsep_pair

added theorem Set.le_einfsep_pi_of_le

added theorem Set.nontrivial_of_einfsep_lt_top

added theorem Set.nontrivial_of_einfsep_ne_top

added theorem Set.nontrivial_of_infsep_pos

added theorem Set.relatively_discrete_of_finite

added theorem Set.subsingleton_of_einfsep_eq_top