case pos
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
⊢ f = 1 ∨ FiniteDimensional 𝕜 E

case neg
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ¬∀ (x : E), f x = 1
⊢ f = 1 ∨ FiniteDimensional 𝕜 E
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
⊢ f = 1 ∨ FiniteDimensional 𝕜 E
by_cases h : ∀ x, f x = 1
case neg.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ¬∀ (x : E), f x = 1
⊢ FiniteDimensional 𝕜 E
case neg
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ¬∀ (x : E), f x = 1
⊢ f = 1 ∨ FiniteDimensional 𝕜 E
apply Or.inr
case neg.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∃ x, f x ≠ 1
⊢ FiniteDimensional 𝕜 E
case neg.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ¬∀ (x : E), f x = 1
⊢ FiniteDimensional 𝕜 E
push_neg at h
case neg.h.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
⊢ FiniteDimensional 𝕜 E
case neg.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∃ x, f x ≠ 1
⊢ FiniteDimensional 𝕜 E
obtain ⟨x, hx⟩ : ∃ x, f x ≠ 1 := h
case neg.h.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this : Function.mulSupport f ∈ 𝓝 x
⊢ FiniteDimensional 𝕜 E
case neg.h.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
⊢ FiniteDimensional 𝕜 E
have : Function.mulSupport f ∈ 𝓝 x := h'f.isOpen_mulSupport.mem_nhds hx
case neg.h.intro.intro.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this : Function.mulSupport f ∈ 𝓝 x
r : ℝ
rpos : 0 < r
hr : Metric.closedBall x r ⊆ Function.mulSupport f
⊢ FiniteDimensional 𝕜 E
case neg.h.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this : Function.mulSupport f ∈ 𝓝 x
⊢ FiniteDimensional 𝕜 E
obtain ⟨r : ℝ, rpos : 0 < r, hr : Metric.closedBall x r ⊆ Function.mulSupport f⟩ :=
  Metric.nhds_basis_closedBall.mem_iff.1 this
case neg.h.intro.intro.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this✝ : Function.mulSupport f ∈ 𝓝 x
r : ℝ
rpos : 0 < r
hr : Metric.closedBall x r ⊆ Function.mulSupport f
this : IsCompact (Metric.closedBall x r)
⊢ FiniteDimensional 𝕜 E
case neg.h.intro.intro.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this : Function.mulSupport f ∈ 𝓝 x
r : ℝ
rpos : 0 < r
hr : Metric.closedBall x r ⊆ Function.mulSupport f
⊢ FiniteDimensional 𝕜 E
have : IsCompact (Metric.closedBall x r) :=
  isCompact_of_isClosed_subset hf Metric.isClosed_ball (hr.trans (subset_mulTSupport _))
no goals
case neg.h.intro.intro.intro
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
x : E
hx : f x ≠ 1
this✝ : Function.mulSupport f ∈ 𝓝 x
r : ℝ
rpos : 0 < r
hr : Metric.closedBall x r ⊆ Function.mulSupport f
this : IsCompact (Metric.closedBall x r)
⊢ FiniteDimensional 𝕜 E
exact finiteDimensional_of_isCompact_closedBall 𝕜 rpos this
case pos.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
⊢ f = 1
case pos
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
⊢ f = 1 ∨ FiniteDimensional 𝕜 E
apply Or.inl
case pos.h.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
x : E
⊢ f x = OfNat.ofNat 1 x
case pos.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
⊢ f = 1
ext x
no goals
case pos.h.h
𝕜 : Type u
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
F : Type w
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : One X
inst✝ : T2Space X
f : E → X
hf : HasCompactMulSupport f
h'f : Continuous f
h : ∀ (x : E), f x = 1
x : E
⊢ f x = OfNat.ofNat 1 x
exact h x