ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : (∑ᶠ (i : ι), ↑(toFun s f i) x) = 1
⊢ ∃ i, 0 < ↑(toFun s f i) x
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
⊢ ∃ i, 0 < ↑(toFun s f i) x
have H := f.sum_eq_one hx
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ¬∃ i, 0 < ↑(toFun s f i) x
⊢ (∑ᶠ (i : ι), ↑(toFun s f i) x) ≠ 1
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : (∑ᶠ (i : ι), ↑(toFun s f i) x) = 1
⊢ ∃ i, 0 < ↑(toFun s f i) x
contrapose! H
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (x_1 : ι), ↑(toFun s f x_1) x ≤ 0
⊢ (∑ᶠ (i : ι), ↑(toFun s f i) x) ≠ 1
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ¬∃ i, 0 < ↑(toFun s f i) x
⊢ (∑ᶠ (i : ι), ↑(toFun s f i) x) ≠ 1
simp_rw [not_exists, not_lt] at H
no goals
ι : Type u
X : Type v
inst✝⁴ : TopologicalSpace X
E : Type ?u.14392
inst✝³ : AddCommMonoid E
inst✝² : SMulWithZero ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set X
f : PartitionOfUnity ι X s
x : X
hx : x ∈ s
H : ∀ (x_1 : ι), ↑(toFun s f x_1) x ≤ 0
⊢ (∑ᶠ (i : ι), ↑(toFun s f i) x) ≠ 1
simpa only [fun i => (H i).antisymm (f.nonneg i x), finsum_zero] using zero_ne_one