case inl
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
⊢ IsClosed ↑(direction ⊥) ↔ IsClosed ↑⊥

case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ↑(direction s) ↔ IsClosed ↑s
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
⊢ IsClosed ↑(direction s) ↔ IsClosed ↑s
rcases s.eq_bot_or_nonempty with (rfl | ⟨x, hx⟩)
case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔
    IsClosed (↑(Homeomorph.symm (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst x))) '' ↑s)
case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ↑(direction s) ↔ IsClosed ↑s
rw [← (IsometryEquiv.vaddConst x).toHomeomorph.symm.isClosed_image,
  AffineSubspace.coe_direction_eq_vsub_set_right hx]
no goals
case inr.intro
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
s : AffineSubspace 𝕜 Q
x : Q
hx : x ∈ ↑s
⊢ IsClosed ((fun x_1 => x_1 -ᵥ x) '' ↑s) ↔
    IsClosed (↑(Homeomorph.symm (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst x))) '' ↑s)
rfl
no goals
case inl
α : Type ?u.597
V : Type ?u.600
P : Type ?u.603
W : Type u_2
Q : Type u_3
inst✝⁸ : SeminormedAddCommGroup V
inst✝⁷ : PseudoMetricSpace P
inst✝⁶ : NormedAddTorsor V P
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : MetricSpace Q
inst✝³ : NormedAddTorsor W Q
𝕜 : Type u_1
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : NormedSpace 𝕜 W
⊢ IsClosed ↑(direction ⊥) ↔ IsClosed ↑⊥
simp [isClosed_singleton]