𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
⊢ interior s ⊆ {x | gauge s x < 1}
intro x hx
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ x ∈ {x | gauge s x < 1}
let f : ℝ → E := fun t => t • x
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
⊢ x ∈ {x | gauge s x < 1}
have hf : Continuous f := by continuity
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
⊢ x ∈ {x | gauge s x < 1}
let s' := f ⁻¹' interior s
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
⊢ x ∈ {x | gauge s x < 1}
have hs' : IsOpen s' := hf.isOpen_preimage _ isOpen_interior
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
⊢ x ∈ {x | gauge s x < 1}
have one_mem : (1 : ℝ) ∈ s' := by simpa only [Set.mem_preimage, one_smul]
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Metric.closedBall 1 ε ⊆ s'
⊢ x ∈ {x | gauge s x < 1}
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
⊢ x ∈ {x | gauge s x < 1}
obtain ⟨ε, hε₀, hε⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs' 1 one_mem)
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
⊢ x ∈ {x | gauge s x < 1}
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Metric.closedBall 1 ε ⊆ s'
⊢ x ∈ {x | gauge s x < 1}
rw [Real.closedBall_eq_Icc] at hε
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ x ∈ {x | gauge s x < 1}
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
⊢ x ∈ {x | gauge s x < 1}
have hε₁ : 0 < 1 + ε := hε₀.trans (lt_one_add ε)
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ x ∈ {x | gauge s x < 1}
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ x ∈ {x | gauge s x < 1}
have : (1 + ε)⁻¹ < 1 := by
  rw [inv_lt_one_iff]
  right
  linarith
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ x ∈ (1 + ε)⁻¹ • s
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ x ∈ {x | gauge s x < 1}
refine' (gauge_le_of_mem (inv_nonneg.2 hε₁.le) _).trans_lt this
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ (1 + ε) • x ∈ s
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ x ∈ (1 + ε)⁻¹ • s
rw [mem_inv_smul_set_iff₀ hε₁.ne']
no goals
case intro.intro
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
this : (1 + ε)⁻¹ < 1
⊢ (1 + ε) • x ∈ s
exact
  interior_subset
    (hε ⟨(sub_le_self _ hε₀.le).trans ((le_add_iff_nonneg_right _).2 hε₀.le), le_rfl⟩)
no goals
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
⊢ Continuous f
continuity
no goals
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
⊢ 1 ∈ s'
simpa only [Set.mem_preimage, one_smul]
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ 1 + ε ≤ 0 ∨ 1 < 1 + ε
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ (1 + ε)⁻¹ < 1
rw [inv_lt_one_iff]
case h
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ 1 < 1 + ε
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ 1 + ε ≤ 0 ∨ 1 < 1 + ε
right
no goals
case h
𝕜 : Type ?u.178960
E : Type u_1
F : Type ?u.178966
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s✝ t : Set E
a : ℝ
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
f : ℝ → E := fun t => t • x
hf : Continuous f
s' : Set ℝ := f ⁻¹' interior s
hs' : IsOpen s'
one_mem : 1 ∈ s'
ε : ℝ
hε₀ : 0 < ε
hε : Icc (1 - ε) (1 + ε) ⊆ s'
hε₁ : 0 < 1 + ε
⊢ 1 < 1 + ε
linarith