no goals
α : Type u
β : Type v
X : Type ?u.195692
ι : Type ?u.195695
inst✝ : PseudoMetricSpace α
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ y ∈ uIcc y' x'
rwa [uIcc_comm]
no goals
α : Type u
β : Type v
X : Type ?u.195692
ι : Type ?u.195695
inst✝ : PseudoMetricSpace α
x y x' y' : ℝ
hx : x ∈ uIcc x' y'
hy : y ∈ uIcc x' y'
⊢ x ∈ uIcc y' x'
rwa [uIcc_comm]