no goals
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi I s) x
classical
rw [← Set.univ_pi_piecewise_univ]
refine' UniqueDiffWithinAt.univ_pi ι E _ _ fun i => _
by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi univ (piecewise I s fun x => univ)) x
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi I s) x
rw [← Set.univ_pi_piecewise_univ]
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
⊢ UniqueDiffWithinAt 𝕜 (piecewise I s (fun x => univ) i) (x i)
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
⊢ UniqueDiffWithinAt 𝕜 (Set.pi univ (piecewise I s fun x => univ)) x
refine' UniqueDiffWithinAt.univ_pi ι E _ _ fun i => _
no goals
𝕜 : Type u_3
inst✝⁹ : NontriviallyNormedField 𝕜
E✝ : Type ?u.151877
inst✝⁸ : NormedAddCommGroup E✝
inst✝⁷ : NormedSpace 𝕜 E✝
F : Type ?u.151972
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
G : Type ?u.152062
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace ℝ G
x✝ y : E✝
s✝ t : Set E✝
ι : Type u_1
inst✝² : Finite ι
E : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
s : (i : ι) → Set (E i)
x : (i : ι) → E i
I : Set ι
h : ∀ (i : ι), i ∈ I → UniqueDiffWithinAt 𝕜 (s i) (x i)
i : ι
⊢ UniqueDiffWithinAt 𝕜 (piecewise I s (fun x => univ) i) (x i)
by_cases hi : i ∈ I <;> simp [*, uniqueDiffWithinAt_univ]