[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ f.linear = (AffineIsometry.linearIsometry f).toLinearMap
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
x✝ : V
⊢ ↑f.linear x✝ = ↑(AffineIsometry.linearIsometry f).toLinearMap x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f✝ f g : P →ᵃⁱ[𝕜] P₂
⊢ (fun f => f.toFun) f = (fun f => f.toFun) g → f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f g : P →ᵃⁱ[𝕜] P₂
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f => f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = (fun f => f.toFun) g →
    { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
toAffineMap✝¹ : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineMap✝¹.linear x‖ = ‖x‖
toAffineMap✝ : P →ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineMap✝.linear x‖ = ‖x‖
⊢ (fun f => f.toFun) { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } =
      (fun f => f.toFun) { toAffineMap := toAffineMap✝, norm_map := norm_map✝ } →
    { toAffineMap := toAffineMap✝¹, norm_map := norm_map✝¹ } = { toAffineMap := toAffineMap✝, norm_map := norm_map✝ }
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ ↑f.toAffineMap = ↑f
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
⊢ Injective toAffineMap
[PROOFSTEP]
rintro ⟨f, _⟩ ⟨g, _⟩ rfl
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f✝ : P →ᵃⁱ[𝕜] P₂
f : P →ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑f.linear x‖ = ‖x‖
norm_map✝ : ∀ (x : V), ‖↑{ toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap.linear x‖ = ‖x‖
⊢ { toAffineMap := f, norm_map := norm_map✝¹ } =
    { toAffineMap := { toAffineMap := f, norm_map := norm_map✝¹ }.toAffineMap, norm_map := norm_map✝ }
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : V →ₗᵢ[𝕜] V₂
⊢ AffineIsometry.linearIsometry (toAffineIsometry f) = f
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : V →ₗᵢ[𝕜] V₂
x✝ : V
⊢ ↑(AffineIsometry.linearIsometry (toAffineIsometry f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ dist (↑f x) (↑f y) = dist x y
[PROOFSTEP]
rw [dist_eq_norm_vsub V₂, dist_eq_norm_vsub V, ← map_vsub, f.linearIsometry.norm_map]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ nndist (↑f x) (↑f y) = nndist x y
[PROOFSTEP]
simp [nndist_dist, (dist_map)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃⁱ[𝕜] P₂
f₁ : P₁ →ᵃⁱ[𝕜] P₂
x y : P
⊢ edist (↑f x) (↑f y) = edist x y
[PROOFSTEP]
simp [edist_dist, (dist_map)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
⊢ e.linear = (AffineIsometryEquiv.linearIsometryEquiv e).toLinearEquiv
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
x✝ : V
⊢ ↑e.linear x✝ = ↑(AffineIsometryEquiv.linearIsometryEquiv e).toLinearEquiv x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e f g : P ≃ᵃⁱ[𝕜] P₂
h : (fun f => f.toFun) f = (fun f => f.toFun) g
x✝ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e g : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h : (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = (fun f => f.toFun) g
x✝ : (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = (fun f => f.invFun) g
⊢ { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h :
  (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
x✝ :
  (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
⊢ { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toAffineEquiv
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
toAffineEquiv✝¹ : P ≃ᵃ[𝕜] P₂
norm_map✝¹ : ∀ (x : V), ‖↑toAffineEquiv✝¹.linear x‖ = ‖x‖
toAffineEquiv✝ : P ≃ᵃ[𝕜] P₂
norm_map✝ : ∀ (x : V), ‖↑toAffineEquiv✝.linear x‖ = ‖x‖
h :
  (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.toFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
x✝ :
  (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝¹, norm_map := norm_map✝¹ } =
    (fun f => f.invFun) { toAffineEquiv := toAffineEquiv✝, norm_map := norm_map✝ }
⊢ toAffineEquiv✝¹ = toAffineEquiv✝
[PROOFSTEP]
simpa [FunLike.coe_injective.eq_iff] using h
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ : P ≃ᵃⁱ[𝕜] P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
⊢ AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h) = e'
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ : P ≃ᵃⁱ[𝕜] P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (mk' e e' p h)) x✝ = ↑e' x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
⊢ ↑(toAffineIsometryEquiv e) = ↑e
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
⊢ AffineIsometryEquiv.linearIsometryEquiv (toAffineIsometryEquiv e) = e
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e : V ≃ₗᵢ[𝕜] V₂
x✝ : V
⊢ ↑(AffineIsometryEquiv.linearIsometryEquiv (toAffineIsometryEquiv e)) x✝ = ↑e x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ↑e = univ
[PROOFSTEP]
rw [← coe_toIsometryEquiv]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
e✝ e : P ≃ᵃⁱ[𝕜] P₂
⊢ range ↑(toIsometryEquiv e) = univ
[PROOFSTEP]
exact IsometryEquiv.range_eq_univ _
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
p : P
⊢ symm (constVSub 𝕜 p) = trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)
[PROOFSTEP]
ext
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
p : P
x✝ : V
⊢ ↑(symm (constVSub 𝕜 p)) x✝ =
    ↑(trans (LinearIsometryEquiv.toAffineIsometryEquiv (LinearIsometryEquiv.neg 𝕜)) (vaddConst 𝕜 p)) x✝
[PROOFSTEP]
rfl
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ Isometry g
[PROOFSTEP]
convert (vaddConst 𝕜 (f p)).symm.isometry.comp (hf.comp (vaddConst 𝕜 p).isometry)
[GOAL]
case h.e'_5
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
f : P → P₂
hf : Isometry f
p : P
g : V → V₂
hg : ∀ (v : V), g v = f (v +ᵥ p) -ᵥ f p
⊢ g = ↑(symm (vaddConst 𝕜 (f p))) ∘ f ∘ ↑(vaddConst 𝕜 p)
[PROOFSTEP]
exact funext hg
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) x = dist y x
[PROOFSTEP]
rw [← (pointReflection 𝕜 x).dist_map y x, pointReflection_self]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) y = ‖bit0 (x -ᵥ y)‖
[PROOFSTEP]
rw [pointReflection_apply, dist_eq_norm_vsub V, vadd_vsub_assoc, bit0]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²¹ : NormedField 𝕜
inst✝²⁰ : SeminormedAddCommGroup V
inst✝¹⁹ : SeminormedAddCommGroup V₁
inst✝¹⁸ : SeminormedAddCommGroup V₂
inst✝¹⁷ : SeminormedAddCommGroup V₃
inst✝¹⁶ : SeminormedAddCommGroup V₄
inst✝¹⁵ : NormedSpace 𝕜 V
inst✝¹⁴ : NormedSpace 𝕜 V₁
inst✝¹³ : NormedSpace 𝕜 V₂
inst✝¹² : NormedSpace 𝕜 V₃
inst✝¹¹ : NormedSpace 𝕜 V₄
inst✝¹⁰ : PseudoMetricSpace P
inst✝⁹ : MetricSpace P₁
inst✝⁸ : PseudoMetricSpace P₂
inst✝⁷ : PseudoMetricSpace P₃
inst✝⁶ : PseudoMetricSpace P₄
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : NormedAddTorsor V₂ P₂
inst✝² : NormedAddTorsor V₃ P₃
inst✝¹ : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝ : TopologicalSpace α
x y : P
⊢ dist (↑(pointReflection 𝕜 x) y) y = ‖2‖ * dist x y
[PROOFSTEP]
rw [dist_pointReflection_self', ← two_smul' 𝕜 (x -ᵥ y), norm_smul, ← dist_eq_norm_vsub V]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²² : NormedField 𝕜
inst✝²¹ : SeminormedAddCommGroup V
inst✝²⁰ : SeminormedAddCommGroup V₁
inst✝¹⁹ : SeminormedAddCommGroup V₂
inst✝¹⁸ : SeminormedAddCommGroup V₃
inst✝¹⁷ : SeminormedAddCommGroup V₄
inst✝¹⁶ : NormedSpace 𝕜 V
inst✝¹⁵ : NormedSpace 𝕜 V₁
inst✝¹⁴ : NormedSpace 𝕜 V₂
inst✝¹³ : NormedSpace 𝕜 V₃
inst✝¹² : NormedSpace 𝕜 V₄
inst✝¹¹ : PseudoMetricSpace P
inst✝¹⁰ : MetricSpace P₁
inst✝⁹ : PseudoMetricSpace P₂
inst✝⁸ : PseudoMetricSpace P₃
inst✝⁷ : PseudoMetricSpace P₄
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddTorsor V₁ P₁
inst✝⁴ : NormedAddTorsor V₂ P₂
inst✝³ : NormedAddTorsor V₃ P₃
inst✝² : NormedAddTorsor V₄ P₄
e : P ≃ᵃⁱ[𝕜] P₂
α : Type u_12
inst✝¹ : TopologicalSpace α
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist (↑(pointReflection ℝ x) y) y = 2 * dist x y
[PROOFSTEP]
rw [dist_pointReflection_self, Real.norm_two]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
inhabit P
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
have :
  (f.linear : V → V₂) =
    (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
      f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph :=
  by
  ext v
  simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
    (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
    (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ ↑f.linear v =
    (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default)))
      v
[PROOFSTEP]
simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
  (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
  (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ Continuous ↑f.linear ↔ Continuous ↑f
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ Continuous
      (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))) ↔
    Continuous ↑f
[PROOFSTEP]
simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
inhabit P
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
have :
  (f.linear : V → V₂) =
    (AffineIsometryEquiv.vaddConst 𝕜 <| f default).toHomeomorph.symm ∘
      f ∘ (AffineIsometryEquiv.vaddConst 𝕜 default).toHomeomorph :=
  by
  ext v
  simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
    (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
    (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
⊢ ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
[PROOFSTEP]
ext v
[GOAL]
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
v : V
⊢ ↑f.linear v =
    (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default)))
      v
[PROOFSTEP]
simp only [(AffineIsometryEquiv.coe_toHomeomorph), Function.comp_apply, (AffineMap.map_vadd), eq_self_iff_true,
  (AffineIsometryEquiv.toHomeomorph_symm), (AffineIsometryEquiv.coe_vaddConst), (vadd_vsub),
  (AffineIsometryEquiv.coe_vaddConst_symm)]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ IsOpenMap ↑f.linear ↔ IsOpenMap ↑f
[PROOFSTEP]
rw [this]
[GOAL]
𝕜 : Type u_1
V : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
V₄ : Type u_6
P₁ : Type u_7
P : Type u_8
P₂ : Type u_9
P₃ : Type u_10
P₄ : Type u_11
inst✝²⁰ : NormedField 𝕜
inst✝¹⁹ : SeminormedAddCommGroup V
inst✝¹⁸ : SeminormedAddCommGroup V₁
inst✝¹⁷ : SeminormedAddCommGroup V₂
inst✝¹⁶ : SeminormedAddCommGroup V₃
inst✝¹⁵ : SeminormedAddCommGroup V₄
inst✝¹⁴ : NormedSpace 𝕜 V
inst✝¹³ : NormedSpace 𝕜 V₁
inst✝¹² : NormedSpace 𝕜 V₂
inst✝¹¹ : NormedSpace 𝕜 V₃
inst✝¹⁰ : NormedSpace 𝕜 V₄
inst✝⁹ : PseudoMetricSpace P
inst✝⁸ : MetricSpace P₁
inst✝⁷ : PseudoMetricSpace P₂
inst✝⁶ : PseudoMetricSpace P₃
inst✝⁵ : PseudoMetricSpace P₄
inst✝⁴ : NormedAddTorsor V P
inst✝³ : NormedAddTorsor V₁ P₁
inst✝² : NormedAddTorsor V₂ P₂
inst✝¹ : NormedAddTorsor V₃ P₃
inst✝ : NormedAddTorsor V₄ P₄
f : P →ᵃ[𝕜] P₂
inhabited_h : Inhabited P
this :
  ↑f.linear =
    ↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
      ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))
⊢ IsOpenMap
      (↑(Homeomorph.symm (AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 (↑f default)))) ∘
        ↑f ∘ ↑(AffineIsometryEquiv.toHomeomorph (AffineIsometryEquiv.vaddConst 𝕜 default))) ↔
    IsOpenMap ↑f
[PROOFSTEP]
simp only [Homeomorph.comp_isOpenMap_iff, Homeomorph.comp_isOpenMap_iff']


[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1
[PROOFSTEP]
rw [inclusionInDoubleDual_norm_eq]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ ≤ 1
[PROOFSTEP]
exact ContinuousLinearMap.norm_id_le
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
⊢ ‖↑(inclusionInDoubleDual 𝕜 E) x‖ ≤ ‖x‖
[PROOFSTEP]
simpa using ContinuousLinearMap.le_of_op_norm_le _ (inclusionInDoubleDual_norm_le 𝕜 E) x
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ LinearMap.SeparatingLeft (dualPairing 𝕜 E)
[PROOFSTEP]
rw [LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.ker_eq_bot]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
⊢ Function.Injective ↑(dualPairing 𝕜 E)
[PROOFSTEP]
exact ContinuousLinearMap.coe_injective
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
classical
by_cases h : x = 0
· simp only [h, hMp, norm_zero]
· obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
  calc
    ‖x‖ = ‖(‖x‖ : 𝕜)‖ := IsROrC.norm_coe_norm.symm
    _ = ‖f x‖ := by rw [hfx]
    _ ≤ M * ‖f‖ := (hM f)
    _ = M := by rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : x = 0
⊢ ‖x‖ ≤ M
[PROOFSTEP]
simp only [h, hMp, norm_zero]
[GOAL]
case neg
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
⊢ ‖x‖ ≤ M
[PROOFSTEP]
obtain ⟨f, hf₁, hfx⟩ : ∃ f : E →L[𝕜] 𝕜, ‖f‖ = 1 ∧ f x = ‖x‖ := exists_dual_vector 𝕜 x h
[GOAL]
case neg.intro.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖x‖ ≤ M
[PROOFSTEP]
calc
  ‖x‖ = ‖(‖x‖ : 𝕜)‖ := IsROrC.norm_coe_norm.symm
  _ = ‖f x‖ := by rw [hfx]
  _ ≤ M * ‖f‖ := (hM f)
  _ = M := by rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ ‖↑‖x‖‖ = ‖↑f x‖
[PROOFSTEP]
rw [hfx]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
M : ℝ
hMp : 0 ≤ M
hM : ∀ (f : Dual 𝕜 E), ‖↑f x‖ ≤ M * ‖f‖
h : ¬x = 0
f : E →L[𝕜] 𝕜
hf₁ : ‖f‖ = 1
hfx : ↑f x = ↑‖x‖
⊢ M * ‖f‖ = M
[PROOFSTEP]
rw [hf₁, mul_one]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
h : ∀ (f : Dual 𝕜 E), ↑f x = 0
f : Dual 𝕜 E
⊢ ‖↑f x‖ ≤ 0 * ‖f‖
[PROOFSTEP]
simp [h f]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∀ (g : Dual 𝕜 E), ↑g x = 0
[PROOFSTEP]
simp [hx]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ x = y ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
[PROOFSTEP]
rw [← sub_eq_zero, eq_zero_iff_forall_dual_eq_zero 𝕜 (x - y)]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x y : E
⊢ (∀ (g : Dual 𝕜 E), ↑g (x - y) = 0) ↔ ∀ (g : Dual 𝕜 E), ↑g x = ↑g y
[PROOFSTEP]
simp [sub_eq_zero]
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
⊢ ∀ (x : E), ‖↑↑src✝ x‖ = ‖x‖
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖↑↑src✝ x‖ = ‖x‖
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖↑↑src✝ x‖ ≤ ‖x‖
[PROOFSTEP]
exact double_dual_bound 𝕜 E x
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖x‖ ≤ ‖↑↑src✝ x‖
[PROOFSTEP]
rw [ContinuousLinearMap.norm_def]
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ‖x‖ ≤ sInf {c | 0 ≤ c ∧ ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖}
[PROOFSTEP]
refine' le_csInf ContinuousLinearMap.bounds_nonempty _
[GOAL]
case a
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
⊢ ∀ (b : ℝ), b ∈ {c | 0 ≤ c ∧ ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖} → ‖x‖ ≤ b
[PROOFSTEP]
rintro c ⟨hc1, hc2⟩
[GOAL]
case a.intro
𝕜 : Type v
inst✝² : IsROrC 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : E →L[𝕜] Dual 𝕜 (Dual 𝕜 E) := inclusionInDoubleDual 𝕜 E
x : E
c : ℝ
hc1 : 0 ≤ c
hc2 : ∀ (x_1 : Dual 𝕜 E), ‖↑(↑↑src✝ x) x_1‖ ≤ c * ‖x_1‖
⊢ ‖x‖ ≤ c
[PROOFSTEP]
exact norm_le_dual_bound 𝕜 x hc1 hc2
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)
[PROOFSTEP]
dsimp only [NormedSpace.polar]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s)
[PROOFSTEP]
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ (x : E) (_ : x ∈ s), {y | ‖↑(↑(dualPairing 𝕜 E) y) x‖ ≤ 1})
[PROOFSTEP]
refine' isClosed_biInter fun z _ => _
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖↑(↑(dualPairing 𝕜 E) y) z‖ ≤ 1}
[PROOFSTEP]
exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed
    ((LinearMap.polar (LinearMap.flip (LinearMap.flip (dualPairing 𝕜 E))) ∘ ↑OrderDual.ofDual)
      (LinearMap.polar (LinearMap.flip (dualPairing 𝕜 E)) s))
[PROOFSTEP]
simpa [LinearMap.flip_flip] using (isClosed_polar _ _).preimage (inclusionInDoubleDual 𝕜 E).continuous
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
by_cases c_zero : c = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
simp only [c_zero, inv_zero, zero_smul]
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : c = 0
⊢ 0 ∈ polar 𝕜 s
[PROOFSTEP]
exact (dualPairing 𝕜 E).flip.zero_mem_polar _
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have eq : ∀ z, ‖c⁻¹ • x' z‖ = ‖c⁻¹‖ * ‖x' z‖ := fun z => norm_smul c⁻¹ _
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have le : ∀ z, z ∈ s → ‖c⁻¹ • x' z‖ ≤ ‖c⁻¹‖ * ‖c‖ := by
  intro z hzs
  rw [eq z]
  apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
⊢ ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
intro z hzs
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
rw [eq z]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
z : E
hzs : z ∈ s
⊢ ‖c⁻¹‖ * ‖↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
[PROOFSTEP]
apply mul_le_mul (le_of_eq rfl) (hc z hzs) (norm_nonneg _) (norm_nonneg _)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
have cancel : ‖c⁻¹‖ * ‖c‖ = 1 := by simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
⊢ ‖c⁻¹‖ * ‖c‖ = 1
[PROOFSTEP]
simp only [c_zero, norm_eq_zero, Ne.def, not_false_iff, inv_mul_cancel, norm_inv]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
x' : Dual 𝕜 E
c : 𝕜
hc : ∀ (z : E), z ∈ s → ‖↑x' z‖ ≤ ‖c‖
c_zero : ¬c = 0
eq : ∀ (z : E), ‖c⁻¹ • ↑x' z‖ = ‖c⁻¹‖ * ‖↑x' z‖
le : ∀ (z : E), z ∈ s → ‖c⁻¹ • ↑x' z‖ ≤ ‖c⁻¹‖ * ‖c‖
cancel : ‖c⁻¹‖ * ‖c‖ = 1
⊢ c⁻¹ • x' ∈ polar 𝕜 s
[PROOFSTEP]
rwa [cancel] at le
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (ball 0 r) ⊆ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
intro x' hx'
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : x' ∈ polar 𝕜 (ball 0 r)
⊢ x' ∈ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
rw [mem_polar_iff] at hx'
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), z ∈ ball 0 r → ‖↑x' z‖ ≤ 1
⊢ x' ∈ closedBall 0 (‖c‖ / r)
[PROOFSTEP]
simp only [polar, mem_setOf, mem_closedBall_zero_iff, mem_ball_zero_iff] at *
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
⊢ ‖x'‖ ≤ ‖c‖ / r
[PROOFSTEP]
have hcr : 0 < ‖c‖ / r := div_pos (zero_lt_one.trans hc) hr
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
⊢ ‖x'‖ ≤ ‖c‖ / r
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_of_shell hr hcr.le hc fun x h₁ h₂ => _
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ ‖↑x' x‖ ≤ ‖c‖ / r * ‖x‖
[PROOFSTEP]
calc
  ‖x' x‖ ≤ 1 := hx' _ h₂
  _ ≤ ‖c‖ / r * ‖x‖ := (inv_pos_le_iff_one_le_mul' hcr).1 (by rwa [inv_div])
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
hx' : ∀ (z : E), ‖z‖ < r → ‖↑x' z‖ ≤ 1
hcr : 0 < ‖c‖ / r
x : E
h₁ : r / ‖c‖ ≤ ‖x‖
h₂ : ‖x‖ < r
⊢ (‖c‖ / r)⁻¹ ≤ ‖x‖
[PROOFSTEP]
rwa [inv_div]
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) = closedBall 0 r⁻¹
[PROOFSTEP]
refine' Subset.antisymm _ (closedBall_inv_subset_polar_closedBall 𝕜)
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ polar 𝕜 (closedBall 0 r) ⊆ closedBall 0 r⁻¹
[PROOFSTEP]
intro x' h
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ x' ∈ closedBall 0 r⁻¹
[PROOFSTEP]
simp only [mem_closedBall_zero_iff]
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
⊢ ‖x'‖ ≤ r⁻¹
[PROOFSTEP]
refine' ContinuousLinearMap.op_norm_le_of_ball hr (inv_nonneg.mpr hr.le) fun z _ => _
[GOAL]
𝕜✝ : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜✝
E✝ : Type u_2
inst✝⁴ : SeminormedAddCommGroup E✝
inst✝³ : NormedSpace 𝕜✝ E✝
𝕜 : Type u_3
E : Type u_4
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
x' : Dual 𝕜 E
h : x' ∈ polar 𝕜 (closedBall 0 r)
z : E
x✝ : z ∈ ball 0 r
⊢ ‖↑x' z‖ ≤ r⁻¹ * ‖z‖
[PROOFSTEP]
simpa only [one_div] using LinearMap.bound_of_ball_bound' hr 1 x'.toLinearMap h z
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhd
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
s_nhd : s ∈ 𝓝 0
a : 𝕜
ha : 1 < ‖a‖
r : ℝ
r_pos : 0 < r
r_ball : ball 0 r ⊆ s
⊢ Metric.Bounded (polar 𝕜 s)
[PROOFSTEP]
exact
  bounded_closedBall.mono
    (((dualPairing 𝕜 E).flip.polar_antitone r_ball).trans <| polar_ball_subset_closedBall_div ha r_pos)


[GOAL]
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f p
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | _h)
[GOAL]
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0
[PROOFSTEP]
exact memℓp_zero_iff.mpr {i : α | f i ≠ 0}.toFinite
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ⊤
[PROOFSTEP]
exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α => ‖f i‖).toFinite)
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < ENNReal.toReal p
⊢ Memℓp f p
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case inr.inr.intro
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < ENNReal.toReal p
val✝ : Fintype α
⊢ Memℓp f p
[PROOFSTEP]
exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
[GOAL]
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | h)
[GOAL]
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E 0 }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ⨆ (i : α), ‖↑Equiv.lpPiLp f i‖ = ⨆ (i : α), ‖↑f i‖
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ (Finset.sum Finset.univ fun i => ‖↑Equiv.lpPiLp f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (Finset.sum Finset.univ fun b => ‖↑f b‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
src✝ : { x // x ∈ lp (fun x => E) ⊤ } ≃+ (α →ᵇ E) := AddEquiv.lpBcf
f : { x // x ∈ lp (fun x => E) ⊤ }
⊢ ‖↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src✝.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                          Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (k : 𝕜) (f : { x // x ∈ lp (fun x => E) ⊤ }),
                      AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                  Equiv.toFun src✝.toEquiv (x + y) =
                                    Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                          (k • f) =
                        AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                  Equiv.toFun src✝.toEquiv (x + y) =
                                    Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                          (k • f)) },
            invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        f‖ =
    ‖f‖
[PROOFSTEP]
simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]
[GOAL]
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
src✝ : { x // x ∈ lp (fun x => E) ⊤ } ≃+ (α →ᵇ E) := AddEquiv.lpBcf
f : { x // x ∈ lp (fun x => E) ⊤ }
⊢ ⨆ (x : α),
      ‖↑(↑{
                  toLinearMap :=
                    {
                      toAddHom :=
                        { toFun := AddEquiv.lpBcf.toEquiv.toFun,
                          map_add' :=
                            (_ :
                              ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                Equiv.toFun src✝.toEquiv (x + y) =
                                  Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) },
                      map_smul' :=
                        (_ :
                          ∀ (k : 𝕜) (f : { x // x ∈ lp (fun x => E) ⊤ }),
                            AddHom.toFun
                                { toFun := src✝.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                        Equiv.toFun src✝.toEquiv (x + y) =
                                          Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                                (k • f) =
                              AddHom.toFun
                                { toFun := src✝.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                        Equiv.toFun src✝.toEquiv (x + y) =
                                          Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                                (k • f)) },
                  invFun := AddEquiv.lpBcf.toEquiv.invFun,
                  left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                  right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
              f)
          x‖ =
    ⨆ (i : α), ‖↑f i‖
[PROOFSTEP]
rfl