[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s✝ : Set M
f✝ : SmoothPartitionOfUnity ι I M s✝
n : ℕ∞
s : Set M
f g : SmoothPartitionOfUnity ι I M s
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s✝ : Set M
f : SmoothPartitionOfUnity ι I M s✝
n : ℕ∞
s : Set M
g : SmoothPartitionOfUnity ι I M s
toFun✝ : ι → C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : ∀ (i : ι) (x : M), 0 ≤ ↑(toFun✝ i) x
sum_eq_one'✝ : ∀ (x : M), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : M), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h : (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun = g.toFun
⊢ mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s✝ : Set M
f : SmoothPartitionOfUnity ι I M s✝
n : ℕ∞
s : Set M
toFun✝¹ : ι → C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'✝¹ : LocallyFinite fun i => support ↑(toFun✝¹ i)
nonneg'✝¹ : ∀ (i : ι) (x : M), 0 ≤ ↑(toFun✝¹ i) x
sum_eq_one'✝¹ : ∀ (x : M), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝¹ i) x = 1
sum_le_one'✝¹ : ∀ (x : M), ∑ᶠ (i : ι), ↑(toFun✝¹ i) x ≤ 1
toFun✝ : ι → C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
locallyFinite'✝ : LocallyFinite fun i => support ↑(toFun✝ i)
nonneg'✝ : ∀ (i : ι) (x : M), 0 ≤ ↑(toFun✝ i) x
sum_eq_one'✝ : ∀ (x : M), x ∈ s → ∑ᶠ (i : ι), ↑(toFun✝ i) x = 1
sum_le_one'✝ : ∀ (x : M), ∑ᶠ (i : ι), ↑(toFun✝ i) x ≤ 1
h :
  (mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹).toFun =
    (mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝).toFun
⊢ mk s toFun✝¹ locallyFinite'✝¹ nonneg'✝¹ sum_eq_one'✝¹ sum_le_one'✝¹ =
    mk s toFun✝ locallyFinite'✝ nonneg'✝ sum_eq_one'✝ sum_le_one'✝
[PROOFSTEP]
congr
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
⊢ ∃ i, 0 < ↑(↑f i) x
[PROOFSTEP]
by_contra h
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
h : ¬∃ i, 0 < ↑(↑f i) x
⊢ False
[PROOFSTEP]
push_neg at h
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
h : ∀ (i : ι), ↑(↑f i) x ≤ 0
⊢ False
[PROOFSTEP]
have H : ∀ i, f i x = 0 := fun i ↦ le_antisymm (h i) (f.nonneg i x)
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H✝ : Type uH
inst✝³ : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H✝ M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
h : ∀ (i : ι), ↑(↑f i) x ≤ 0
H : ∀ (i : ι), ↑(↑f i) x = 0
⊢ False
[PROOFSTEP]
have := f.sum_eq_one hx
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H✝ : Type uH
inst✝³ : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H✝ M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
h : ∀ (i : ι), ↑(↑f i) x ≤ 0
H : ∀ (i : ι), ↑(↑f i) x = 0
this : ∑ᶠ (i : ι), ↑(↑f i) x = 1
⊢ False
[PROOFSTEP]
simp_rw [H] at this
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H✝ : Type uH
inst✝³ : TopologicalSpace H✝
I : ModelWithCorners ℝ E H✝
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H✝ M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
f : SmoothPartitionOfUnity ι I M s
n : ℕ∞
x : M
hx : x ∈ s
h : ∀ (i : ι), ↑(↑f i) x ≤ 0
H : ∀ (i : ι), ↑(↑f i) x = 0
this : ∑ᶠ (i : ι), 0 = 1
⊢ False
[PROOFSTEP]
simpa
[GOAL]
ι : Type uι
E✝ : Type uE
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace ℝ E✝
inst✝¹¹ : FiniteDimensional ℝ E✝
F : Type uF
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
H✝ : Type uH
inst✝⁸ : TopologicalSpace H✝
I✝ : ModelWithCorners ℝ E✝ H✝
M✝ : Type uM
inst✝⁷ : TopologicalSpace M✝
inst✝⁶ : ChartedSpace H✝ M✝
inst✝⁵ : SmoothManifoldWithCorners I✝ M✝
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ↑(↑f i)
i : ι
⊢ LocallyFinite fun i => mulSupport ((fun x => 1) - ↑(↑f i))
[PROOFSTEP]
simp only [Pi.sub_def, mulSupport_one_sub]
[GOAL]
ι : Type uι
E✝ : Type uE
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace ℝ E✝
inst✝¹¹ : FiniteDimensional ℝ E✝
F : Type uF
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
H✝ : Type uH
inst✝⁸ : TopologicalSpace H✝
I✝ : ModelWithCorners ℝ E✝ H✝
M✝ : Type uM
inst✝⁷ : TopologicalSpace M✝
inst✝⁶ : ChartedSpace H✝ M✝
inst✝⁵ : SmoothManifoldWithCorners I✝ M✝
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type uH
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
f : BumpCovering ι M s
hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ↑(↑f i)
i : ι
⊢ LocallyFinite fun i => support fun x => ↑(↑f i) x
[PROOFSTEP]
exact f.locallyFinite
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
haveI : LocallyCompactSpace H := I.locally_compact
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this : LocallyCompactSpace H
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
haveI : NormalSpace M := normal_of_paracompact_t2
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
have hB := fun x hx => SmoothBumpFunction.nhds_basis_support I (hU x hx)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set hs hB with ⟨ι, c, f, hf, hsub', hfin⟩
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hf : ∀ (a : ι), c a ∈ s ∧ tsupport ↑(f a) ⊆ U (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
choose hcs hfU using hf
[GOAL]
case intro.intro.intro.intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
rcases exists_subset_iUnion_closed_subset hs (fun i => (f i).isOpen_support) (fun x _ => hfin.point_finite x) hsub' with
  ⟨V, hsV, hVc, hVf⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
choose r hrR hr using fun i => (f i).exists_r_pos_lt_subset_ball (hVc i) (hVf i)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (chartAt H (c i)).toLocalEquiv.source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
⊢ ∃ ι f, IsSubordinate f U
[PROOFSTEP]
refine' ⟨ι, ⟨c, fun i => (f i).updateRIn (r i) (hrR i), hcs, _, fun x hx => _⟩, fun i => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (chartAt H (c i)).toLocalEquiv.source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
⊢ LocallyFinite fun i => support ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) i)
[PROOFSTEP]
simpa only [SmoothBumpFunction.support_updateRIn]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (chartAt H (c i)).toLocalEquiv.source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
x : M
hx : x ∈ s
⊢ ∃ i, ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
refine' (mem_iUnion.1 <| hsV hx).imp fun i hi => _
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (chartAt H (c i)).toLocalEquiv.source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
x : M
hx : x ∈ s
i : ι
hi : x ∈ V i
⊢ ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) i) =ᶠ[𝓝 x] 1
[PROOFSTEP]
exact ((f i).updateRIn _ _).eventuallyEq_one_of_dist_lt ((f i).support_subset_source <| hVf _ hi) (hr i hi).2
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_3
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι✝ I M s
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
hs : IsClosed s
hU : ∀ (x : M), x ∈ s → U x ∈ 𝓝 x
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
hB : ∀ (x : M), x ∈ s → HasBasis (𝓝 x) (fun f => tsupport ↑f ⊆ U x) fun f => support ↑f
ι : Type uM
c : ι → M
f : (a : ι) → SmoothBumpFunction I (c a)
hsub' : s ⊆ ⋃ (a : ι), support ↑(f a)
hfin : LocallyFinite fun a => support ↑(f a)
hcs : ∀ (a : ι), c a ∈ s
hfU : ∀ (a : ι), tsupport ↑(f a) ⊆ U (c a)
V : ι → Set M
hsV : s ⊆ iUnion V
hVc : ∀ (i : ι), IsClosed (V i)
hVf : ∀ (i : ι), V i ⊆ support ↑(f i)
r : ι → ℝ
hrR : ∀ (i : ι), r i ∈ Ioo 0 (f i).rOut
hr :
  ∀ (i : ι),
    V i ⊆
      (chartAt H (c i)).toLocalEquiv.source ∩ ↑(extChartAt I (c i)) ⁻¹' Metric.ball (↑(extChartAt I (c i)) (c i)) (r i)
i : ι
⊢ tsupport
      ↑(toFun s
          (mk s c (fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) hcs
            (_ :
              LocallyFinite fun i =>
                support ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) i))
            (_ :
              ∀ (x : M),
                x ∈ s →
                  ∃ a, ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) a) =ᶠ[𝓝 x] 1))
          i) ⊆
    U
      (SmoothBumpCovering.c s
        (mk s c (fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) hcs
          (_ :
            LocallyFinite fun i =>
              support ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) i))
          (_ :
            ∀ (x : M),
              x ∈ s →
                ∃ a, ↑((fun i => SmoothBumpFunction.updateRIn (f i) (r i) (_ : r i ∈ Ioo 0 (f i).rOut)) a) =ᶠ[𝓝 x] 1))
        i)
[PROOFSTEP]
simpa only [SmoothBumpFunction.support_updateRIn, tsupport] using hfU i
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(toFun s fs i) x = 1
⊢ x ∈ support ↑(toFun s fs i)
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(toFun s fs i) x = 1
⊢ x ∈ (extChartAt I (c s fs i)).source
[PROOFSTEP]
rw [extChartAt_source]
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
i : ι
x : M
h : ↑(toFun s fs i) x = 1
⊢ x ∈ (chartAt H (c s fs i)).toLocalEquiv.source
[PROOFSTEP]
exact fs.mem_chartAt_source_of_eq_one h
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ x ∈ support ↑(toFun s fs (ind fs x hx))
[PROOFSTEP]
simp [fs.apply_ind x hx]
[GOAL]
ι : Type uι
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : FiniteDimensional ℝ E
F : Type uF
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type uH
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
s : Set M
U : M → Set M
fs : SmoothBumpCovering ι I M s
inst✝ : T2Space M
i : ι
x : M
⊢ ∃ t,
    ↑(↑(toSmoothPartitionOfUnity fs) i) =ᶠ[𝓝 x]
      ↑(toFun s fs i) * ∏ j in Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(toFun s fs j))
[PROOFSTEP]
simpa using fs.toBumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq i x
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
have : ∀ x ∈ t, sᶜ ∈ 𝓝 x := fun x hx => hs.isOpen_compl.mem_nhds (disjoint_right.1 hd hx)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
rcases SmoothBumpCovering.exists_isSubordinate I ht this with ⟨ι, f, hf⟩
[GOAL]
case intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
set g := f.toSmoothPartitionOfUnity
[GOAL]
case intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := SmoothBumpCovering.toSmoothPartitionOfUnity f
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
refine' ⟨⟨_, g.smooth_sum⟩, fun x hx => _, fun x => g.sum_eq_one, fun x => ⟨g.sum_nonneg x, g.sum_le_one x⟩⟩
[GOAL]
case intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := SmoothBumpCovering.toSmoothPartitionOfUnity f
x : M
hx : x ∈ s
⊢ ↑{ val := fun x => ∑ᶠ (i : ι), ↑(↑g i) x, property := (_ : Smooth I 𝓘(ℝ, ℝ) fun x => ∑ᶠ (i : ι), ↑(↑g i) x) } x =
    OfNat.ofNat 0 x
[PROOFSTEP]
suffices ∀ i, g i x = 0 by simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
[GOAL]
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this✝ : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := SmoothBumpCovering.toSmoothPartitionOfUnity f
x : M
hx : x ∈ s
this : ∀ (i : ι), ↑(↑g i) x = 0
⊢ ↑{ val := fun x => ∑ᶠ (i : ι), ↑(↑g i) x, property := (_ : Smooth I 𝓘(ℝ, ℝ) fun x => ∑ᶠ (i : ι), ↑(↑g i) x) } x =
    OfNat.ofNat 0 x
[PROOFSTEP]
simp only [this, ContMDiffMap.coeFn_mk, finsum_zero, Pi.zero_apply]
[GOAL]
case intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := SmoothBumpCovering.toSmoothPartitionOfUnity f
x : M
hx : x ∈ s
⊢ ∀ (i : ι), ↑(↑g i) x = 0
[PROOFSTEP]
refine' fun i => f.toSmoothPartitionOfUnity_zero_of_zero _
[GOAL]
case intro.intro
ι✝ : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
this : ∀ (x : M), x ∈ t → sᶜ ∈ 𝓝 x
ι : Type uM
f : SmoothBumpCovering ι I M t
hf : SmoothBumpCovering.IsSubordinate f fun x => sᶜ
g : SmoothPartitionOfUnity ι I M t := SmoothBumpCovering.toSmoothPartitionOfUnity f
x : M
hx : x ∈ s
i : ι
⊢ ↑(SmoothBumpCovering.toFun t f i) x = 0
[PROOFSTEP]
exact nmem_support.1 (subset_compl_comm.1 (hf.support_subset i) hx)
[GOAL]
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
i : ι
s : Set M
j : ι
⊢ Smooth I 𝓘(ℝ, ℝ) ↑(↑(BumpCovering.single i s) j)
[PROOFSTEP]
rcases eq_or_ne j i with (rfl | h)
[GOAL]
case inl
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
s : Set M
j : ι
⊢ Smooth I 𝓘(ℝ, ℝ) ↑(↑(BumpCovering.single j s) j)
[PROOFSTEP]
simp only [smooth_one, ContinuousMap.coe_one, BumpCovering.coe_single, Pi.single_eq_same]
[GOAL]
case inr
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : SmoothManifoldWithCorners I M
i : ι
s : Set M
j : ι
h : j ≠ i
⊢ Smooth I 𝓘(ℝ, ℝ) ↑(↑(BumpCovering.single i s) j)
[PROOFSTEP]
simp only [smooth_zero, BumpCovering.coe_single, Pi.single_eq_of_ne h, ContinuousMap.coe_zero]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
haveI : LocallyCompactSpace H := I.locally_compact
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this : LocallyCompactSpace H
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
haveI : LocallyCompactSpace M := ChartedSpace.locallyCompact H M
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this✝ : LocallyCompactSpace H
this : LocallyCompactSpace M
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
haveI : NormalSpace M := normal_of_paracompact_t2
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
have := BumpCovering.exists_isSubordinate_of_prop (Smooth I 𝓘(ℝ)) ?_ hs U ho hU
[GOAL]
case refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this✝² : LocallyCompactSpace H
this✝¹ : LocallyCompactSpace M
this✝ : NormalSpace M
this : ∃ f, (∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ↑(↑f i)) ∧ BumpCovering.IsSubordinate f U
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
rcases this with ⟨f, hf, hfU⟩
[GOAL]
case refine_2.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
f : BumpCovering ι M s
hf : ∀ (i : ι), Smooth I 𝓘(ℝ, ℝ) ↑(↑f i)
hfU : BumpCovering.IsSubordinate f U
⊢ ∃ f, IsSubordinate f U
[PROOFSTEP]
exact ⟨f.toSmoothPartitionOfUnity hf, hfU.toSmoothPartitionOfUnity hf⟩
[GOAL]
case refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s ⊆ ⋃ (i : ι), U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
⊢ ∀ (s t : Set M),
    IsClosed s →
      IsClosed t → Disjoint s t → ∃ f, Smooth I 𝓘(ℝ, ℝ) ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
intro s t hs ht hd
[GOAL]
case refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ (i : ι), U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
rcases exists_smooth_zero_one_of_closed I hs ht hd with ⟨f, hf⟩
[GOAL]
case refine_1.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s✝ : Set M
hs✝ : IsClosed s✝
U : ι → Set M
ho : ∀ (i : ι), IsOpen (U i)
hU : s✝ ⊆ ⋃ (i : ι), U i
this✝¹ : LocallyCompactSpace H
this✝ : LocallyCompactSpace M
this : NormalSpace M
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hf : EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) ↑f ∧ EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : M), ↑f x ∈ Icc 0 1
[PROOFSTEP]
exact ⟨f, f.smooth, hf⟩
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
⊢ ∃ f, IsSubordinate f fun x => (chartAt H ↑x).toLocalEquiv.source
[PROOFSTEP]
apply exists_isSubordinate _ hs _ (fun i ↦ (chartAt H _).open_source) (fun x hx ↦ ?_)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
s : Set M
hs : IsClosed s
x : M
hx : x ∈ s
⊢ x ∈ ⋃ (i : ↑s), (chartAt H ↑i).toLocalEquiv.source
[PROOFSTEP]
exact mem_iUnion_of_mem ⟨x, hx⟩ (mem_chart_source H x)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
⊢ ∃ f, IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
[PROOFSTEP]
apply exists_isSubordinate _ isClosed_univ _ (fun i ↦ (chartAt H _).open_source) (fun x _ ↦ ?_)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : T2Space M
inst✝ : SigmaCompactSpace M
x : M
x✝ : x ∈ univ
⊢ x ∈ ⋃ (i : M), (chartAt H i).toLocalEquiv.source
[PROOFSTEP]
exact mem_iUnion_of_mem x (mem_chart_source H x)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
Hloc : ∀ (x : M), ∃ U, U ∈ 𝓝 x ∧ ∃ g, ContMDiffOn I 𝓘(ℝ, F) n g U ∧ ∀ (y : M), y ∈ U → g y ∈ t y
⊢ ∃ g, ∀ (x : M), ↑g x ∈ t x
[PROOFSTEP]
choose U hU g hgs hgt using Hloc
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
⊢ ∃ g, ∀ (x : M), ↑g x ∈ t x
[PROOFSTEP]
obtain ⟨f, hf⟩ :=
  SmoothPartitionOfUnity.exists_isSubordinate I isClosed_univ (fun x => interior (U x)) (fun x => isOpen_interior)
    fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => interior (U x)
⊢ ∃ g, ∀ (x : M), ↑g x ∈ t x
[PROOFSTEP]
refine'
  ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
      hf.contMDiff_finsum_smul (fun i => isOpen_interior) fun i => (hgs i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ _) (ht _)⟩
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
ht : ∀ (x : M), Convex ℝ (t x)
U : M → Set M
hU : ∀ (x : M), U x ∈ 𝓝 x
g : M → M → F
hgs : ∀ (x : M), ContMDiffOn I 𝓘(ℝ, F) n (g x) (U x)
hgt : ∀ (x y : M), y ∈ U x → g x y ∈ t y
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => interior (U x)
x i : M
hi : ↑(↑f i) x ≠ 0
⊢ x ∈ U i
[PROOFSTEP]
exact interior_subset (hf _ <| subset_closure hi)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : FiniteDimensional ℝ E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
H : Type uH
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type uM
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H M✝
inst✝⁶ : SmoothManifoldWithCorners I M✝
inst✝⁵ : SigmaCompactSpace M✝
inst✝⁴ : T2Space M✝
t : M✝ → Set F
n : ℕ∞
M : Type u_1
inst✝³ : EMetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : M), 0 < ↑δ x) ∧ ∀ (i : ι) (x : M), x ∈ K i → EMetric.closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
[PROOFSTEP]
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι M] using
  exists_smooth_forall_mem_convex_of_local_const I EMetric.exists_forall_closedBall_subset_aux₂
    (EMetric.exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : FiniteDimensional ℝ E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
H : Type uH
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type uM
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H M✝
inst✝⁶ : SmoothManifoldWithCorners I M✝
inst✝⁵ : SigmaCompactSpace M✝
inst✝⁴ : T2Space M✝
t : M✝ → Set F
n : ℕ∞
M : Type u_1
inst✝³ : MetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : M), 0 < ↑δ x) ∧ ∀ (i : ι) (x : M), x ∈ K i → closedBall x (↑δ x) ⊆ U i
[PROOFSTEP]
rcases Emetric.exists_smooth_forall_closedBall_subset I hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
[GOAL]
case intro.intro
ι : Type uι
E : Type uE
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : FiniteDimensional ℝ E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
H : Type uH
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type uM
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H M✝
inst✝⁶ : SmoothManifoldWithCorners I M✝
inst✝⁵ : SigmaCompactSpace M✝
inst✝⁴ : T2Space M✝
t : M✝ → Set F
n : ℕ∞
M : Type u_1
inst✝³ : MetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), 0 < ↑δ x
hδ : ∀ (i : ι) (x : M), x ∈ K i → EMetric.closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
⊢ ∃ δ, (∀ (x : M), 0 < ↑δ x) ∧ ∀ (i : ι) (x : M), x ∈ K i → closedBall x (↑δ x) ⊆ U i
[PROOFSTEP]
refine' ⟨δ, hδ0, fun i x hx => _⟩
[GOAL]
case intro.intro
ι : Type uι
E : Type uE
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : FiniteDimensional ℝ E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
H : Type uH
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type uM
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H M✝
inst✝⁶ : SmoothManifoldWithCorners I M✝
inst✝⁵ : SigmaCompactSpace M✝
inst✝⁴ : T2Space M✝
t : M✝ → Set F
n : ℕ∞
M : Type u_1
inst✝³ : MetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), 0 < ↑δ x
hδ : ∀ (i : ι) (x : M), x ∈ K i → EMetric.closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
⊢ closedBall x (↑δ x) ⊆ U i
[PROOFSTEP]
rw [← Metric.emetric_closedBall (hδ0 _).le]
[GOAL]
case intro.intro
ι : Type uι
E : Type uE
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : FiniteDimensional ℝ E
F : Type uF
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
H : Type uH
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M✝ : Type uM
inst✝⁸ : TopologicalSpace M✝
inst✝⁷ : ChartedSpace H M✝
inst✝⁶ : SmoothManifoldWithCorners I M✝
inst✝⁵ : SigmaCompactSpace M✝
inst✝⁴ : T2Space M✝
t : M✝ → Set F
n : ℕ∞
M : Type u_1
inst✝³ : MetricSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SmoothManifoldWithCorners I M
inst✝ : SigmaCompactSpace M
K U : ι → Set M
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C^⊤⟮I, M; 𝓘(ℝ, ℝ), ℝ⟯
hδ0 : ∀ (x : M), 0 < ↑δ x
hδ : ∀ (i : ι) (x : M), x ∈ K i → EMetric.closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
i : ι
x : M
hx : x ∈ K i
⊢ EMetric.closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
[PROOFSTEP]
exact hδ i x hx
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
[PROOFSTEP]
have h's : IsOpen (I.symm ⁻¹' s) := I.continuous_symm.isOpen_preimage _ hs
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
[PROOFSTEP]
rcases h's.exists_smooth_support_eq with ⟨f, f_supp, f_diff, f_range⟩
[GOAL]
case intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑(ModelWithCorners.symm I) ⁻¹' s
f_diff : ContDiff ℝ ⊤ f
f_range : range f ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1
[PROOFSTEP]
refine ⟨f ∘ I, ?_, ?_, ?_⟩
[GOAL]
case intro.intro.intro.refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑(ModelWithCorners.symm I) ⁻¹' s
f_diff : ContDiff ℝ ⊤ f
f_range : range f ⊆ Icc 0 1
⊢ support (f ∘ ↑I) = s
[PROOFSTEP]
rw [support_comp_eq_preimage, f_supp, ← preimage_comp]
[GOAL]
case intro.intro.intro.refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑(ModelWithCorners.symm I) ⁻¹' s
f_diff : ContDiff ℝ ⊤ f
f_range : range f ⊆ Icc 0 1
⊢ ↑(ModelWithCorners.symm I) ∘ ↑I ⁻¹' s = s
[PROOFSTEP]
simp only [ModelWithCorners.symm_comp_self, preimage_id_eq, id_eq]
[GOAL]
case intro.intro.intro.refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑(ModelWithCorners.symm I) ⁻¹' s
f_diff : ContDiff ℝ ⊤ f
f_range : range f ⊆ Icc 0 1
⊢ Smooth I 𝓘(ℝ, ℝ) (f ∘ ↑I)
[PROOFSTEP]
exact f_diff.comp_contMDiff contMDiff_model
[GOAL]
case intro.intro.intro.refine_3
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set H
hs : IsOpen s
h's : IsOpen (↑(ModelWithCorners.symm I) ⁻¹' s)
f : E → ℝ
f_supp : support f = ↑(ModelWithCorners.symm I) ⁻¹' s
f_diff : ContDiff ℝ ⊤ f
f_range : range f ⊆ Icc 0 1
⊢ range (f ∘ ↑I) ⊆ Icc 0 1
[PROOFSTEP]
exact Subset.trans (range_comp_subset_range _ _) f_range
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
rcases SmoothPartitionOfUnity.exists_isSubordinate_chartAt_source I M with ⟨f, hf⟩
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
have A :
  ∀ (c : M),
    ∃ g : H → ℝ,
      g.support = (chartAt H c).target ∩ (chartAt H c).symm ⁻¹' s ∧ Smooth I 𝓘(ℝ) g ∧ Set.range g ⊆ Set.Icc 0 1 :=
  by
  intro i
  apply IsOpen.exists_msmooth_support_eq_aux
  exact LocalHomeomorph.preimage_open_of_open_symm _ hs
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
⊢ ∀ (c : M),
    ∃ g,
      support g = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s ∧
        Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1
[PROOFSTEP]
intro i
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
i : M
⊢ ∃ g,
    support g = (chartAt H i).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H i)) ⁻¹' s ∧
      Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1
[PROOFSTEP]
apply IsOpen.exists_msmooth_support_eq_aux
[GOAL]
case hs
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
i : M
⊢ IsOpen ((chartAt H i).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H i)) ⁻¹' s)
[PROOFSTEP]
exact LocalHomeomorph.preimage_open_of_open_symm _ hs
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
A :
  ∀ (c : M),
    ∃ g,
      support g = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s ∧
        Smooth I 𝓘(ℝ, ℝ) g ∧ range g ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
choose g g_supp g_diff hg using A
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
have h'g : ∀ c x, 0 ≤ g c x := fun c x ↦ (hg c (mem_range_self (f := g c) x)).1
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
have h''g : ∀ c x, 0 ≤ f c x * g c (chartAt H c x) := fun c x ↦ mul_nonneg (f.nonneg c x) (h'g c _)
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ ∃ f, support f = s ∧ Smooth I 𝓘(ℝ, ℝ) f ∧ ∀ (x : M), 0 ≤ f x
[PROOFSTEP]
refine ⟨fun x ↦ ∑ᶠ c, f c x * g c (chartAt H c x), ?_, ?_, ?_⟩
[GOAL]
case intro.refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ (support fun x => ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)) = s
[PROOFSTEP]
refine support_eq_iff.2 ⟨fun x hx ↦ ?_, fun x hx ↦ ?_⟩
[GOAL]
case intro.refine_1.refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
⊢ ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x) ≠ 0
[PROOFSTEP]
apply ne_of_gt
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
⊢ 0 < ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)
[PROOFSTEP]
have B : ∃ c, 0 < f c x * g c (chartAt H c x) :=
  by
  obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)
  refine ⟨c, mul_pos hc ?_⟩
  apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)
  rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]
  have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)
  simp [(chartAt H c).left_inv (hf c Hx), hx, (chartAt H c).map_source (hf c Hx)]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
⊢ ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
[PROOFSTEP]
obtain ⟨c, hc⟩ : ∃ c, 0 < f c x := f.exists_pos_of_mem (mem_univ x)
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < ↑(↑f c) x
⊢ ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
[PROOFSTEP]
refine ⟨c, mul_pos hc ?_⟩
[GOAL]
case intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < ↑(↑f c) x
⊢ 0 < g c (↑(chartAt H c) x)
[PROOFSTEP]
apply lt_of_le_of_ne (h'g _ _) (Ne.symm _)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < ↑(↑f c) x
⊢ g c (↑(chartAt H c) x) ≠ 0
[PROOFSTEP]
rw [← mem_support, g_supp, ← mem_preimage, preimage_inter]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < ↑(↑f c) x
⊢ x ∈
    ↑(chartAt H c) ⁻¹' (chartAt H c).toLocalEquiv.target ∩
      ↑(chartAt H c) ⁻¹' (↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s)
[PROOFSTEP]
have Hx : x ∈ tsupport (f c) := subset_tsupport _ (ne_of_gt hc)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
c : M
hc : 0 < ↑(↑f c) x
Hx : x ∈ tsupport ↑(↑f c)
⊢ x ∈
    ↑(chartAt H c) ⁻¹' (chartAt H c).toLocalEquiv.target ∩
      ↑(chartAt H c) ⁻¹' (↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s)
[PROOFSTEP]
simp [(chartAt H c).left_inv (hf c Hx), hx, (chartAt H c).map_source (hf c Hx)]
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
B : ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ 0 < ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)
[PROOFSTEP]
apply finsum_pos' (fun c ↦ h''g c x) B
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
B : ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ Set.Finite (support fun c => ↑(↑f c) x * g c (↑(chartAt H c) x))
[PROOFSTEP]
apply (f.locallyFinite.point_finite x).subset
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
B : ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ (support fun c => ↑(↑f c) x * g c (↑(chartAt H c) x)) ⊆ {b | x ∈ support ↑(↑f b)}
[PROOFSTEP]
apply compl_subset_compl.2
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
B : ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ (fun x_1 => ↑(↑f x_1) x = 0) ⊆ fun x_1 => (fun c => ↑(↑f c) x * g c (↑(chartAt H c) x)) x_1 = 0
[PROOFSTEP]
rintro c (hc : f c x = 0)
[GOAL]
case intro.refine_1.refine_1.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : x ∈ s
B : ∃ c, 0 < ↑(↑f c) x * g c (↑(chartAt H c) x)
c : M
hc : ↑(↑f c) x = 0
⊢ c ∈ fun x_1 => (fun c => ↑(↑f c) x * g c (↑(chartAt H c) x)) x_1 = 0
[PROOFSTEP]
simpa only [mul_eq_zero] using Or.inl hc
[GOAL]
case intro.refine_1.refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
⊢ ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
apply finsum_eq_zero_of_forall_eq_zero
[GOAL]
case intro.refine_1.refine_2.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
⊢ ∀ (x_1 : M), ↑(↑f x_1) x * g x_1 (↑(chartAt H x_1) x) = 0
[PROOFSTEP]
intro c
[GOAL]
case intro.refine_1.refine_2.h
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
by_cases Hx : x ∈ tsupport (f c)
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : x ∈ tsupport ↑(↑f c)
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
suffices g c (chartAt H c x) = 0 by simp only [this, mul_zero]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : x ∈ tsupport ↑(↑f c)
this : g c (↑(chartAt H c) x) = 0
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
simp only [this, mul_zero]
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : x ∈ tsupport ↑(↑f c)
⊢ g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
rw [← nmem_support, g_supp, ← mem_preimage, preimage_inter]
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : x ∈ tsupport ↑(↑f c)
⊢ ¬x ∈
      ↑(chartAt H c) ⁻¹' (chartAt H c).toLocalEquiv.target ∩
        ↑(chartAt H c) ⁻¹' (↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s)
[PROOFSTEP]
contrapose! hx
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ↑(↑f c)
hx :
  x ∈
    ↑(chartAt H c) ⁻¹' (chartAt H c).toLocalEquiv.target ∩
      ↑(chartAt H c) ⁻¹' (↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s)
⊢ x ∈ s
[PROOFSTEP]
simp only [mem_inter_iff, mem_preimage, (chartAt H c).left_inv (hf c Hx)] at hx
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x c : M
Hx : x ∈ tsupport ↑(↑f c)
hx : ↑(chartAt H c) x ∈ (chartAt H c).toLocalEquiv.target ∧ x ∈ s
⊢ x ∈ s
[PROOFSTEP]
exact hx.2
[GOAL]
case neg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : ¬x ∈ tsupport ↑(↑f c)
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
have : x ∉ support (f c) := by contrapose! Hx; exact subset_tsupport _ Hx
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : ¬x ∈ tsupport ↑(↑f c)
⊢ ¬x ∈ support ↑(↑f c)
[PROOFSTEP]
contrapose! Hx
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : x ∈ support ↑(↑f c)
⊢ x ∈ tsupport ↑(↑f c)
[PROOFSTEP]
exact subset_tsupport _ Hx
[GOAL]
case neg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : ¬x ∈ tsupport ↑(↑f c)
this : ¬x ∈ support ↑(↑f c)
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
rw [nmem_support] at this
[GOAL]
case neg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
hx : ¬x ∈ s
c : M
Hx : ¬x ∈ tsupport ↑(↑f c)
this : ↑(↑f c) x = 0
⊢ ↑(↑f c) x * g c (↑(chartAt H c) x) = 0
[PROOFSTEP]
simp [this]
[GOAL]
case intro.refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ Smooth I 𝓘(ℝ, ℝ) fun x => ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)
[PROOFSTEP]
apply SmoothPartitionOfUnity.smooth_finsum_smul
[GOAL]
case intro.refine_2.hg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ ∀ (i x : M), x ∈ tsupport ↑(↑f i) → SmoothAt I 𝓘(ℝ, ℝ) (fun x => g i (↑(chartAt H i) x)) x
[PROOFSTEP]
intro c x hx
[GOAL]
case intro.refine_2.hg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
c x : M
hx : x ∈ tsupport ↑(↑f c)
⊢ SmoothAt I 𝓘(ℝ, ℝ) (fun x => g c (↑(chartAt H c) x)) x
[PROOFSTEP]
apply (g_diff c (chartAt H c x)).comp
[GOAL]
case intro.refine_2.hg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
c x : M
hx : x ∈ tsupport ↑(↑f c)
⊢ ContMDiffAt I I ⊤ (↑(chartAt H c)) x
[PROOFSTEP]
exact contMDiffAt_of_mem_maximalAtlas (SmoothManifoldWithCorners.chart_mem_maximalAtlas I _) (hf c hx)
[GOAL]
case intro.refine_3
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
⊢ ∀ (x : M), 0 ≤ (fun x => ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)) x
[PROOFSTEP]
intro x
[GOAL]
case intro.refine_3
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t : M → Set F
n : ℕ∞
s : Set M
hs : IsOpen s
f : SmoothPartitionOfUnity M I M univ
hf : SmoothPartitionOfUnity.IsSubordinate f fun x => (chartAt H x).toLocalEquiv.source
g : M → H → ℝ
g_supp : ∀ (c : M), support (g c) = (chartAt H c).toLocalEquiv.target ∩ ↑(LocalHomeomorph.symm (chartAt H c)) ⁻¹' s
g_diff : ∀ (c : M), Smooth I 𝓘(ℝ, ℝ) (g c)
hg : ∀ (c : M), range (g c) ⊆ Icc 0 1
h'g : ∀ (c : M) (x : H), 0 ≤ g c x
h''g : ∀ (c x : M), 0 ≤ ↑(↑f c) x * g c (↑(chartAt H c) x)
x : M
⊢ 0 ≤ (fun x => ∑ᶠ (c : M), ↑(↑f c) x * g c (↑(chartAt H c) x)) x
[PROOFSTEP]
apply finsum_nonneg (fun c ↦ h''g c x)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
rcases hs.exists_msmooth_support_eq I with ⟨f, f_supp, f_diff, f_pos⟩
[GOAL]
case intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
rcases ht.isOpen_compl.exists_msmooth_support_eq I with ⟨g, g_supp, g_diff, g_pos⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
have A : ∀ x, 0 < f x + g x := by
  intro x
  by_cases xs : x ∈ support f
  · have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
    linarith [g_pos x]
  · have : 0 < g x := by
      apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
      rw [← mem_support, g_supp]
      contrapose! xs
      simp at xs
      exact h.trans f_supp.symm.subset xs
    linarith [f_pos x]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
⊢ ∀ (x : M), 0 < f x + g x
[PROOFSTEP]
intro x
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
⊢ 0 < f x + g x
[PROOFSTEP]
by_cases xs : x ∈ support f
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ support f
⊢ 0 < f x + g x
[PROOFSTEP]
have : 0 < f x := lt_of_le_of_ne (f_pos x) (Ne.symm xs)
[GOAL]
case pos
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ support f
this : 0 < f x
⊢ 0 < f x + g x
[PROOFSTEP]
linarith [g_pos x]
[GOAL]
case neg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ support f
⊢ 0 < f x + g x
[PROOFSTEP]
have : 0 < g x := by
  apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
  rw [← mem_support, g_supp]
  contrapose! xs
  simp at xs
  exact h.trans f_supp.symm.subset xs
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ support f
⊢ 0 < g x
[PROOFSTEP]
apply lt_of_le_of_ne (g_pos x) (Ne.symm ?_)
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ support f
⊢ g x ≠ 0
[PROOFSTEP]
rw [← mem_support, g_supp]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ support f
⊢ x ∈ tᶜ
[PROOFSTEP]
contrapose! xs
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ tᶜ
⊢ x ∈ support f
[PROOFSTEP]
simp at xs
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : x ∈ t
⊢ x ∈ support f
[PROOFSTEP]
exact h.trans f_supp.symm.subset xs
[GOAL]
case neg
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
x : M
xs : ¬x ∈ support f
this : 0 < g x
⊢ 0 < f x + g x
[PROOFSTEP]
linarith [f_pos x]
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ support f = s ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
refine
  ⟨fun x ↦ f x / (f x + g x), ?_, ?_, ?_, ?_⟩
    -- show that `f / (f + g)` is smooth
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_1
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ Smooth I 𝓘(ℝ, ℝ) fun x => f x / (f x + g x)
[PROOFSTEP]
exact
  f_diff.div₀ (f_diff.add g_diff)
    (fun x ↦ ne_of_gt (A x))
      -- show that the range is included in `[0, 1]`
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ (range fun x => f x / (f x + g x)) ⊆ Icc 0 1
[PROOFSTEP]
refine range_subset_iff.2 (fun x ↦ ⟨div_nonneg (f_pos x) (A x).le, ?_⟩)
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_2
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x / (f x + g x) ≤ 1
[PROOFSTEP]
apply div_le_one_of_le _ (A x).le
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ f x ≤ f x + g x
[PROOFSTEP]
simpa only [le_add_iff_nonneg_right] using g_pos x
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_3
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ (support fun x => f x / (f x + g x)) = s
[PROOFSTEP]
have B : support (fun x ↦ f x + g x) = univ := eq_univ_of_forall (fun x ↦ (A x).ne')
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_3
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
B : (support fun x => f x + g x) = univ
⊢ (support fun x => f x / (f x + g x)) = s
[PROOFSTEP]
simp only [support_div, f_supp, B, inter_univ]
  -- show that the function equals one exactly on `t`
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_4
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
⊢ ∀ (x : M), x ∈ t ↔ (fun x => f x / (f x + g x)) x = 1
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.intro.intro.intro.intro.refine_4
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsOpen s
ht : IsClosed t
h : t ⊆ s
f : M → ℝ
f_supp : support f = s
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_pos : ∀ (x : M), 0 ≤ f x
g : M → ℝ
g_supp : support g = tᶜ
g_diff : Smooth I 𝓘(ℝ, ℝ) g
g_pos : ∀ (x : M), 0 ≤ g x
A : ∀ (x : M), 0 < f x + g x
x : M
⊢ x ∈ t ↔ (fun x => f x / (f x + g x)) x = 1
[PROOFSTEP]
simp [div_eq_one_iff_eq (A x).ne', self_eq_add_right, ← nmem_support, g_supp]
[GOAL]
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
rcases exists_msmooth_support_eq_eq_one_iff I hs.isOpen_compl ht hd.subset_compl_left with ⟨f, f_diff, f_range, fs, ft⟩
[GOAL]
case intro.intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∃ f, Smooth I 𝓘(ℝ, ℝ) f ∧ range f ⊆ Icc 0 1 ∧ (∀ (x : M), x ∈ s ↔ f x = 0) ∧ ∀ (x : M), x ∈ t ↔ f x = 1
[PROOFSTEP]
refine ⟨f, f_diff, f_range, ?_, ft⟩
[GOAL]
case intro.intro.intro.intro
ι : Type uι
E : Type uE
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : FiniteDimensional ℝ E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : SmoothManifoldWithCorners I M
inst✝¹ : SigmaCompactSpace M
inst✝ : T2Space M
t✝ : M → Set F
n : ℕ∞
s t : Set M
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
f : M → ℝ
f_diff : Smooth I 𝓘(ℝ, ℝ) f
f_range : range f ⊆ Icc 0 1
fs : support f = sᶜ
ft : ∀ (x : M), x ∈ t ↔ f x = 1
⊢ ∀ (x : M), x ∈ s ↔ f x = 0
[PROOFSTEP]
simp [← nmem_support, fs]