case intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
⊢ (⨆ (i : ι), edist (f i) (g i)) ≠ ⊤
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
⊢ (⨆ (i : ι), edist (f i) (g i)) ≠ ⊤
cases nonempty_fintype ι
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
⊢ (⨆ (i : ι), edist (f i) (g i)) ≠ ⊤
case intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
⊢ (⨆ (i : ι), edist (f i) (g i)) ≠ ⊤
obtain ⟨M, hM⟩ := Fintype.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ edist (f i) (g i) ≤ ↑M
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
⊢ (⨆ (i : ι), edist (f i) (g i)) ≠ ⊤
refine' ne_of_lt ((iSup_le fun i => _).trans_lt (@ENNReal.coe_lt_top M))
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ ↑{ val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ ↑M
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ edist (f i) (g i) ≤ ↑M
simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]
no goals
case intro.intro
p : ℝ≥0∞
𝕜 : Type ?u.36838
𝕜' : Type ?u.36841
ι✝ : Type ?u.36844
α✝ : ι✝ → Type ?u.36849
β : ι✝ → Type ?u.36854
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_1
inst✝¹ : Finite ι
α : ι → Type u_2
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ ↑{ val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ ↑M
exact_mod_cast hM i