case inl
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f

case inr.inl
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ⊤ β
⊢ edist f g = edist g f

case inr.inr
p : ℝ≥0∞
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f g = edist g f
p : ℝ≥0∞
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
⊢ edist f g = edist g f
rcases p.trichotomy with (rfl | rfl | h)
no goals
case inl
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f
simp only [edist_eq_card, eq_comm, Ne.def]
no goals
case inr.inl
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ⊤ β
⊢ edist f g = edist g f
simp only [edist_eq_iSup, edist_comm]
no goals
case inr.inr
p : ℝ≥0∞
𝕜 : Type ?u.15998
𝕜' : Type ?u.16001
ι : Type u_1
α : ι → Type ?u.16009
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f g = edist g f
simp only [edist_eq_sum h, edist_comm]