α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
  have : LipschitzOnWith K (fun x : α => f x i) s :=
    LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
      (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
  exact this.extend_real
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
choose g hg using this
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x y : α
⊢ (dist (fun i => g i x) fun i => g i y) ≤ ↑K * dist x y

case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ EqOn f (fun x i => g i x) s
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
refine' ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => _, _⟩
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith K (fun x => f x i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
have : LipschitzOnWith K (fun x : α => f x i) s :=
  LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
    (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith K (fun x => f x i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
exact this.extend_real
no goals
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x y : α
⊢ (dist (fun i => g i x) fun i => g i y) ≤ ↑K * dist x y
exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i => g i x) x
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ EqOn f (fun x i => g i x) s
intro x hx
case refine'_2.h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i => g i x) x i
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i => g i x) x
ext1 i
no goals
case refine'_2.h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i => g i x) x i
exact (hg i).2 hx