English
For all x in X and y in Y, the distance between the cross-pair is at least 1.
Русский
Для всех x∈X и y∈Y расстояние между кросс-парой не меньше 1.
LaTeX
$$$ 1 \le Sum.dist (Sum.inr y) (Sum.inl x). $$$
Lean4
/-- The distance on the disjoint union indeed defines a metric space. All the distance properties
follow from our choice of the distance. The harder work is to show that the uniform structure
defined by the distance coincides with the disjoint union uniform structure. -/
def metricSpaceSum : MetricSpace (X ⊕ Y) where
dist := Sum.dist
dist_self x := by cases x <;> simp only [Sum.dist, dist_self]
dist_comm := Sum.dist_comm
dist_triangle
| .inl p, .inl q, .inl r => dist_triangle p q r
| .inl p, .inr q, _ => by
simp only [Sum.dist_eq_glueDist p q]
exact glueDist_triangle _ _ _ (by simp) _ _ _
| _, .inl q, .inr r => by
simp only [Sum.dist_eq_glueDist q r]
exact glueDist_triangle _ _ _ (by simp) _ _ _
| .inr p, _, .inl r => by
simp only [Sum.dist_eq_glueDist r p]
exact glueDist_triangle _ _ _ (by simp) _ _ _
| .inr p, .inr q, .inr r => dist_triangle p q r
eq_of_dist_eq_zero {p q}
h := by
rcases p with p | p <;> rcases q with q | q
· rw [eq_of_dist_eq_zero h]
· exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist p q).symm.trans h)
· exact eq_of_glueDist_eq_zero _ _ _ one_pos _ _ ((Sum.dist_eq_glueDist q p).symm.trans h)
· rw [eq_of_dist_eq_zero h]
toUniformSpace := Sum.instUniformSpace
uniformity_dist := uniformity_dist_of_mem_uniformity _ _ Sum.mem_uniformity
