𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
inhabit P
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
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)]
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
rw [this]
no goals
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
simp only [Homeomorph.comp_continuous_iff, Homeomorph.comp_continuous_iff']
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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))
ext v
no goals
case h
𝕜 : Type u_1
V : Type u_2
V₁ : Type ?u.2232204
V₂ : Type u_4
V₃ : Type ?u.2232210
V₄ : Type ?u.2232213
P₁ : Type ?u.2232216
P : Type u_3
P₂ : Type u_5
P₃ : Type ?u.2232225
P₄ : Type ?u.2232228
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
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)]