Theorem: isCompact_segment (RMT4/to_mathlib.lean)

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : TopologicalAddGroup 𝕜
inst✝⁵ : CompactIccSpace 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ IsCompact (segment 𝕜 x y)
Tactic:
simpa only [segment_eq_image] using isCompact_Icc.image (by continuity)
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : TopologicalAddGroup 𝕜
inst✝⁵ : CompactIccSpace 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y
Tactic:
continuity
State after:
no goals