Real

📁 Source: Mathlib/Topology/MetricSpace/Pseudo/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems dist_le_of_mem_Icc, dist_le_of_mem_Icc_01, dist_le_of_mem_pi_Icc, dist_le_of_mem_uIcc, dist_left_le_of_mem_uIcc, dist_right_le_of_mem_uIcc	6
Total	6

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_le_of_mem_Icc 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace instSub	—	abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_nonpos covariant_swap_add_of_covariant_add LE.le.trans neg_sub dist_le_of_mem_uIcc Set.Icc_subset_uIcc
dist_le_of_mem_Icc_01 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instZero instOne	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace	—	sub_zero dist_le_of_mem_Icc
dist_le_of_mem_pi_Icc 📖	mathematical	Set Set.instMembership Set.Icc Pi.preorder Real instPreorder	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpacePi pseudoMetricSpace	—	dist_pi_le_iff dist_nonneg LE.le.trans dist_le_of_mem_uIcc Set.Icc_subset_uIcc dist_le_pi_dist
dist_le_of_mem_uIcc 📖	mathematical	Real Set Set.instMembership Set.uIcc lattice	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace	—	Set.abs_sub_le_of_uIcc_subset_uIcc instIsOrderedAddMonoid Set.uIcc_subset_uIcc Set.uIcc_comm
dist_left_le_of_mem_uIcc 📖	mathematical	Real Set Set.instMembership Set.uIcc lattice	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace	—	dist_comm Set.abs_sub_left_of_mem_uIcc instIsOrderedAddMonoid
dist_right_le_of_mem_uIcc 📖	mathematical	Real Set Set.instMembership Set.uIcc lattice	instLE Dist.dist PseudoMetricSpace.toDist pseudoMetricSpace	—	dist_comm Set.abs_sub_right_of_mem_uIcc instIsOrderedAddMonoid

---

← Back to Index