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

case inr.inl
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ⊤ β
⊢ edist f f = 0

case inr.inr
p : ℝ≥0∞
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f f = 0
p : ℝ≥0∞
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
⊢ edist f f = 0
rcases p.trichotomy with (rfl | rfl | h)
no goals
case inl
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp 0 β
⊢ edist f f = 0
simp [edist_eq_card]
no goals
case inr.inl
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ⊤ β
⊢ edist f f = 0
simp [edist_eq_iSup]
no goals
case inr.inr
p : ℝ≥0∞
𝕜 : Type ?u.8431
𝕜' : Type ?u.8434
ι : Type u_1
α : ι → Type ?u.8442
β : ι → Type u_2
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f f = 0
simp [edist_eq_sum h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]