Infsep

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

Statistics

Metric	Count
Definitions einfsep, infsep	2
Theorems coe_infsep, coe_infsep_of_offDiag_empty, coe_infsep_of_offDiag_nonempty, infsep_pos_iff_nontrivial, infsep_zero_iff_subsingleton, einfsep, einfsep_exists_of_nontrivial, einfsep_pos, infsep, infsep_exists_of_nontrivial, infsep_of_nontrivial, infsep_pos_iff_nontrivial, infsep_zero_iff_subsingleton, relatively_discrete, coe_einfsep, einfsep_exists_of_finite, einfsep_lt_top, einfsep_ne_top, infsep_anti, infsep_eq_iInf, infsep_exists_of_finite, infsep_lt_iff, infsep_of_fintype, le_infsep, le_infsep_iff, einfsep, infsep_zero, einfsep_anti, einfsep_empty, einfsep_eq_iInf, einfsep_eq_top_iff, einfsep_iUnion_mem_option, einfsep_insert, einfsep_insert_le, einfsep_le_edist_of_mem, einfsep_le_of_mem_of_edist_le, einfsep_lt_iff, einfsep_lt_top, einfsep_lt_top_iff, einfsep_ne_top, einfsep_ne_top_iff, einfsep_of_fintype, einfsep_pair, einfsep_pair_eq_inf, einfsep_pair_le_left, einfsep_pair_le_right, einfsep_pos, einfsep_pos_of_finite, einfsep_singleton, einfsep_top, einfsep_triple, einfsep_zero, infsep_empty, infsep_eq_iInf, infsep_le_dist_of_mem, infsep_le_of_mem_of_edist_le, infsep_nonneg, infsep_of_fintype, infsep_pair, infsep_pair_eq_toReal, infsep_pair_le_toReal_inf, infsep_pos, infsep_pos_iff_nontrivial_of_finite, infsep_singleton, infsep_triple, infsep_zero, infsep_zero_iff_subsingleton_of_finite, le_edist_of_le_einfsep, le_edist_of_le_infsep, le_einfsep, le_einfsep_iff, le_einfsep_image_iff, le_einfsep_of_forall_dist_le, le_einfsep_pair, le_einfsep_pi_of_le, nontrivial_of_einfsep_lt_top, nontrivial_of_einfsep_ne_top, nontrivial_of_infsep_pos, relatively_discrete_of_finite, subsingleton_of_einfsep_eq_top	80
Total	82

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_infsep 📖	mathematical	—	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SetLike.coe Finset instSetLike Real Nonempty offDiag decidableNonempty inf' Real.instSemilatticeInf Dist.dist PseudoMetricSpace.toDist Real.instZero	—	Set.offDiag_nonempty coe_offDiag coe_nonempty Set.Nontrivial.infsep_of_fintype Set.toFinset_congr inf'_congr toFinset_coe Set.Subsingleton.infsep_zero Set.not_nontrivial_iff Function.mt
coe_infsep_of_offDiag_empty 📖	mathematical	offDiag Finset instEmptyCollection	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SetLike.coe instSetLike Real Real.instZero	—	coe_infsep not_nonempty_iff_eq_empty
coe_infsep_of_offDiag_nonempty 📖	mathematical	Nonempty offDiag	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace SetLike.coe Finset instSetLike inf' Real Real.instSemilatticeInf Dist.dist PseudoMetricSpace.toDist	—	coe_infsep
infsep_pos_iff_nontrivial 📖	mathematical	—	Real Real.instLT Real.instZero Set.infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace SetLike.coe Finset instSetLike Set.Nontrivial	—	Set.infsep_pos_iff_nontrivial_of_finite Finite.of_fintype
infsep_zero_iff_subsingleton 📖	mathematical	—	Set.infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace SetLike.coe Finset instSetLike Real Real.instZero Set.Subsingleton	—	Set.infsep_zero_iff_subsingleton_of_finite Finite.of_fintype

Set

Definitions

Name	Category	Theorems
einfsep 📖	CompOp	37 math math: Finite.einfsep, einfsep_of_fintype, einfsep_pair_le_left, le_einfsep_of_forall_dist_le, einfsep_lt_top_iff, einfsep_zero, Finset.coe_einfsep, einfsep_le_edist_of_mem, einfsep_anti, einfsep_eq_top_iff, einfsep_insert, einfsep_lt_iff, infsep_zero, einfsep_insert_le, einfsep_top, le_einfsep, le_einfsep_iff, einfsep_singleton, einfsep_le_of_mem_of_edist_le, einfsep_lt_top, einfsep_eq_iInf, einfsep_pair_eq_inf, einfsep_pos_of_finite, einfsep_pair_le_right, le_einfsep_image_iff, einfsep_triple, einfsep_pair, le_einfsep_pair, infsep_pos, Finite.einfsep_pos, Nontrivial.einfsep_exists_of_finite, Nontrivial.einfsep_lt_top, einfsep_iUnion_mem_option, Subsingleton.einfsep, einfsep_empty, einfsep_pos, Finite.einfsep_exists_of_nontrivial
infsep 📖	CompOp	33 math math: infsep_zero_iff_subsingleton_of_finite, Finset.infsep_pos_iff_nontrivial, Finite.infsep_of_nontrivial, Finset.coe_infsep_of_offDiag_nonempty, Nontrivial.infsep_of_fintype, infsep_le_of_mem_of_edist_le, Finite.infsep, Nontrivial.infsep_eq_iInf, Finite.infsep_pos_iff_nontrivial, infsep_eq_iInf, infsep_pair, Nontrivial.infsep_lt_iff, infsep_pos_iff_nontrivial_of_finite, infsep_zero, infsep_of_fintype, Finite.infsep_exists_of_nontrivial, infsep_nonneg, Finset.coe_infsep, Nontrivial.infsep_anti, Finite.infsep_zero_iff_subsingleton, Finset.coe_infsep_of_offDiag_empty, Nontrivial.infsep_exists_of_finite, infsep_singleton, infsep_pair_le_toReal_inf, infsep_triple, infsep_empty, infsep_le_dist_of_mem, Finset.infsep_zero_iff_subsingleton, infsep_pair_eq_toReal, Nontrivial.le_infsep, infsep_pos, Subsingleton.infsep_zero, Nontrivial.le_infsep_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
einfsep_anti 📖	mathematical	Set instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep	—	le_einfsep einfsep_le_edist_of_mem
einfsep_empty 📖	mathematical	—	einfsep Set instEmptyCollection Top.top ENNReal instTopENNReal	—	Subsingleton.einfsep subsingleton_empty
einfsep_eq_iInf 📖	mathematical	—	einfsep iInf ENNReal Elem offDiag ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder EDist.edist Set instMembership	—	eq_of_forall_le_iff
einfsep_eq_top_iff 📖	mathematical	—	einfsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Top.top ENNReal instTopENNReal Subsingleton	—	subsingleton_of_einfsep_eq_top Subsingleton.einfsep
einfsep_iUnion_mem_option 📖	mathematical	—	einfsep iUnion iInf ENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	iUnion_congr_Prop iUnion_of_empty instIsEmptyFalse iUnion_empty einfsep_empty iInf_congr_Prop iInf_neg iInf_top iUnion_iUnion_eq_right iInf_iInf_eq_right
einfsep_insert 📖	mathematical	—	einfsep PseudoEMetricSpace.toEDist Set instInsert ENNReal ENNReal.instMin iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder instMembership EDist.edist	—	le_antisymm le_min einfsep_insert_le einfsep_anti subset_insert iInf_le_of_le iInf₂_le PseudoEMetricSpace.edist_comm einfsep_le_edist_of_mem
einfsep_insert_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Set instInsert iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder instMembership EDist.edist	—	einfsep_le_edist_of_mem mem_insert mem_insert_of_mem
einfsep_le_edist_of_mem 📖	mathematical	Set instMembership	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep EDist.edist	—	le_edist_of_le_einfsep le_rfl
einfsep_le_of_mem_of_edist_le 📖	mathematical	Set instMembership ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist	einfsep	—	le_trans einfsep_le_edist_of_mem
einfsep_lt_iff 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Set instMembership EDist.edist	—	—
einfsep_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Top.top instTopENNReal Set instMembership EDist.edist	—	—
einfsep_lt_top_iff 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder einfsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Top.top instTopENNReal Nontrivial	—	nontrivial_of_einfsep_lt_top Nontrivial.einfsep_lt_top
einfsep_ne_top 📖	mathematical	—	Set instMembership	—	—
einfsep_ne_top_iff 📖	mathematical	—	Nontrivial	—	nontrivial_of_einfsep_ne_top Nontrivial.einfsep_ne_top
einfsep_of_fintype 📖	mathematical	—	einfsep Finset.inf ENNReal Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.instOrderTop toFinset offDiag fintypeOffDiag EDist.edist	—	eq_of_forall_le_iff
einfsep_pair 📖	mathematical	—	einfsep PseudoEMetricSpace.toEDist Set instInsert instSingletonSet EDist.edist	—	min_self PseudoEMetricSpace.edist_comm einfsep_pair_eq_inf
einfsep_pair_eq_inf 📖	mathematical	—	einfsep Set instInsert instSingletonSet ENNReal ENNReal.instMin EDist.edist	—	le_antisymm le_inf einfsep_pair_le_left einfsep_pair_le_right le_einfsep_pair
einfsep_pair_le_left 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Set instInsert instSingletonSet EDist.edist	—	einfsep_le_edist_of_mem mem_insert mem_insert_of_mem mem_singleton
einfsep_pair_le_right 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Set instInsert instSingletonSet EDist.edist	—	pair_comm einfsep_pair_le_left
einfsep_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal einfsep Preorder.toLE EDist.edist	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd einfsep_zero
einfsep_pos_of_finite 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal einfsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	nonempty_fintype Nontrivial.einfsep_exists_of_finite edist_pos WithTop.top_pos Subsingleton.einfsep not_nontrivial_iff
einfsep_singleton 📖	mathematical	—	einfsep Set instSingletonSet Top.top ENNReal instTopENNReal	—	Subsingleton.einfsep subsingleton_singleton
einfsep_top 📖	mathematical	—	einfsep Top.top ENNReal instTopENNReal EDist.edist	—	—
einfsep_triple 📖	mathematical	—	einfsep PseudoEMetricSpace.toEDist Set instInsert instSingletonSet ENNReal ENNReal.instMin EDist.edist	—	einfsep_insert iInf_insert iInf_singleton einfsep_singleton inf_top_eq ciInf_pos
einfsep_zero 📖	mathematical	—	einfsep ENNReal instZeroENNReal Set instMembership Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist	—	ENNReal.instCanonicallyOrderedAdd
infsep_empty 📖	mathematical	—	infsep Set instEmptyCollection Real Real.instZero	—	Subsingleton.infsep_zero subsingleton_empty
infsep_eq_iInf 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Real Nontrivial iInf Elem offDiag Real.instInfSet Dist.dist PseudoMetricSpace.toDist Set instMembership Real.instZero	—	dist_nonneg eq_of_forall_le_iff Nontrivial.le_infsep_iff le_ciInf_set_iff offDiag_nonempty Subsingleton.infsep_zero not_nontrivial_iff
infsep_le_dist_of_mem 📖	mathematical	Set instMembership	Real Real.instLE infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Dist.dist PseudoMetricSpace.toDist	—	le_edist_of_le_infsep le_rfl
infsep_le_of_mem_of_edist_le 📖	mathematical	Set instMembership Real Real.instLE Dist.dist PseudoMetricSpace.toDist	infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	—	le_trans infsep_le_dist_of_mem
infsep_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero infsep	—	ENNReal.toReal_nonneg
infsep_of_fintype 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Real Nontrivial Finset.inf' Real.instSemilatticeInf toFinset offDiag fintypeOffDiag Dist.dist PseudoMetricSpace.toDist Real.instZero	—	eq_of_forall_le_iff Nontrivial.le_infsep_iff Subsingleton.infsep_zero not_nontrivial_iff
infsep_pair 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Set instInsert instSingletonSet Dist.dist PseudoMetricSpace.toDist	—	infsep_pair_eq_toReal edist_dist ENNReal.toReal_ofReal dist_nonneg
infsep_pair_eq_toReal 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist Set instInsert instSingletonSet ENNReal.toReal EDist.edist	—	pair_eq_singleton infsep_singleton PseudoEMetricSpace.edist_self infsep.eq_1 einfsep_pair
infsep_pair_le_toReal_inf 📖	mathematical	—	Real Real.instLE infsep Set instInsert instSingletonSet ENNReal.toReal ENNReal ENNReal.instMin EDist.edist	—	einfsep_pair_eq_inf
infsep_pos 📖	mathematical	—	Real Real.instLT Real.instZero infsep ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal einfsep Top.top instTopENNReal	—	—
infsep_pos_iff_nontrivial_of_finite 📖	mathematical	—	Real Real.instLT Real.instZero infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Nontrivial	—	infsep_pos einfsep_lt_top_iff einfsep_pos_of_finite
infsep_singleton 📖	mathematical	—	infsep Set instSingletonSet Real Real.instZero	—	Subsingleton.infsep_zero subsingleton_singleton
infsep_triple 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Set instInsert instSingletonSet Real Real.instMin Dist.dist PseudoMetricSpace.toDist	—	einfsep_triple ENNReal.toReal_inf edist_ne_top dist_edist
infsep_zero 📖	mathematical	—	infsep Real Real.instZero einfsep ENNReal instZeroENNReal Top.top instTopENNReal	—	infsep.eq_1 ENNReal.toReal_eq_zero_iff
infsep_zero_iff_subsingleton_of_finite 📖	mathematical	—	infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real Real.instZero Subsingleton	—	infsep_zero einfsep_eq_top_iff LT.lt.ne' einfsep_pos_of_finite
le_edist_of_le_einfsep 📖	mathematical	Set instMembership ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep	EDist.edist	—	le_einfsep_iff
le_edist_of_le_infsep 📖	mathematical	Set instMembership Real Real.instLE infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	Dist.dist PseudoMetricSpace.toDist	—	Nontrivial.le_infsep_iff le_trans Subsingleton.infsep_zero not_nontrivial_iff dist_nonneg
le_einfsep 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder EDist.edist	einfsep	—	le_einfsep_iff
le_einfsep_iff 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep EDist.edist	—	—
le_einfsep_image_iff 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep image EDist.edist	—	—
le_einfsep_of_forall_dist_le 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.ofReal einfsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	—	le_einfsep ENNReal.ofReal_le_ofReal edist_dist
le_einfsep_pair 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instMin EDist.edist einfsep Set instInsert instSingletonSet	—	—
le_einfsep_pi_of_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder einfsep PseudoEMetricSpace.toEDist	instEDistForall pi univ	—	le_einfsep Function.ne_iff le_trans le_einfsep_iff mem_univ_pi edist_le_pi_edist
nontrivial_of_einfsep_lt_top 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder einfsep Top.top instTopENNReal	Nontrivial	—	einfsep_lt_top
nontrivial_of_einfsep_ne_top 📖	mathematical	—	Nontrivial	—	nontrivial_of_einfsep_lt_top lt_top_iff_ne_top
nontrivial_of_infsep_pos 📖	mathematical	Real Real.instLT Real.instZero infsep	Nontrivial	—	Mathlib.Tactic.Contrapose.contrapose₁ lt_irrefl Subsingleton.infsep_zero not_nontrivial_iff
relatively_discrete_of_finite 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	einfsep_pos einfsep_pos_of_finite
subsingleton_of_einfsep_eq_top 📖	mathematical	einfsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Top.top ENNReal instTopENNReal	Subsingleton	—	of_not_not edist_ne_top einfsep_top

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
einfsep 📖	mathematical	—	Set.einfsep Finset.inf ENNReal Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.instOrderTop toFinset Set.offDiag offDiag EDist.edist	—	eq_of_forall_le_iff offDiag
einfsep_exists_of_nontrivial 📖	mathematical	Set.Nontrivial	Set Set.instMembership Set.einfsep EDist.edist	—	Set.Nontrivial.einfsep_exists_of_finite Finite.of_fintype
einfsep_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.einfsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	Set.einfsep_pos_of_finite Finite.of_fintype
infsep 📖	mathematical	—	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Real Set.Nontrivial Finset.inf' Real.instSemilatticeInf toFinset Set.offDiag offDiag Dist.dist PseudoMetricSpace.toDist Real.instZero	—	offDiag eq_of_forall_le_iff Set.Nontrivial.le_infsep_iff Set.Subsingleton.infsep_zero Set.not_nontrivial_iff
infsep_exists_of_nontrivial 📖	mathematical	Set.Nontrivial	Set Set.instMembership Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Dist.dist PseudoMetricSpace.toDist	—	Set.Nontrivial.infsep_exists_of_finite Finite.of_fintype
infsep_of_nontrivial 📖	mathematical	Set.Nontrivial	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Finset.inf' Real Real.instSemilatticeInf toFinset Set.offDiag offDiag Dist.dist PseudoMetricSpace.toDist	—	offDiag infsep
infsep_pos_iff_nontrivial 📖	mathematical	—	Real Real.instLT Real.instZero Set.infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Set.Nontrivial	—	Set.infsep_pos_iff_nontrivial_of_finite Finite.of_fintype
infsep_zero_iff_subsingleton 📖	mathematical	—	Set.infsep PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Real Real.instZero Set.Subsingleton	—	Set.infsep_zero_iff_subsingleton_of_finite Finite.of_fintype
relatively_discrete 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	Set.relatively_discrete_of_finite Finite.of_fintype

Set.Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_einfsep 📖	mathematical	—	Set.einfsep SetLike.coe Finset Finset.instSetLike Finset.inf ENNReal Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ENNReal.instOrderTop Finset.offDiag EDist.edist	—	Set.einfsep_of_fintype Set.toFinset_congr Finset.toFinset_coe

Set.Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
einfsep_exists_of_finite 📖	mathematical	Set.Nontrivial	Set Set.instMembership Set.einfsep EDist.edist	—	nonempty_fintype Set.einfsep_of_fintype Finset.exists_mem_eq_inf
einfsep_lt_top 📖	mathematical	Set.Nontrivial	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Set.einfsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Top.top instTopENNReal	—	lt_top_iff_ne_top einfsep_ne_top
einfsep_ne_top 📖	—	Set.Nontrivial	—	—	Mathlib.Tactic.Contrapose.contrapose₃ Set.subsingleton_of_einfsep_eq_top
infsep_anti 📖	mathematical	Set.Nontrivial Set Set.instHasSubset	Real Real.instLE Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	—	ENNReal.toReal_mono einfsep_ne_top Set.einfsep_anti
infsep_eq_iInf 📖	mathematical	Set.Nontrivial	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace iInf Real Set.Elem Set.offDiag Real.instInfSet Dist.dist PseudoMetricSpace.toDist Set Set.instMembership	—	Set.infsep_eq_iInf
infsep_exists_of_finite 📖	mathematical	Set.Nontrivial	Set Set.instMembership Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Dist.dist PseudoMetricSpace.toDist	—	nonempty_fintype infsep_of_fintype Finset.exists_mem_eq_inf'
infsep_lt_iff 📖	mathematical	Set.Nontrivial	Real Real.instLT Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Set Set.instMembership Dist.dist PseudoMetricSpace.toDist	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_and_eq le_infsep_iff
infsep_of_fintype 📖	mathematical	Set.Nontrivial	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Finset.inf' Real Real.instSemilatticeInf Set.toFinset Set.offDiag Set.fintypeOffDiag Dist.dist PseudoMetricSpace.toDist	—	Set.infsep_of_fintype
le_infsep 📖	mathematical	Set.Nontrivial Real Real.instLE Dist.dist PseudoMetricSpace.toDist	Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace	—	le_infsep_iff
le_infsep_iff 📖	mathematical	Set.Nontrivial	Real Real.instLE Set.infsep PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace Dist.dist PseudoMetricSpace.toDist	—	ENNReal.ofReal_le_iff_le_toReal einfsep_ne_top edist_dist ENNReal.ofReal_le_ofReal_iff dist_nonneg

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
einfsep 📖	mathematical	Set.Subsingleton	Set.einfsep Top.top ENNReal instTopENNReal	—	Set.einfsep_top
infsep_zero 📖	mathematical	Set.Subsingleton	Set.infsep Real Real.instZero	—	Set.infsep_zero einfsep

---

← Back to Index