English
If s0 and s1 are compact and disjoint, there exist compactly supported nonnegative functions f0,f1 with f0=1 on s0, f1=1 on s1, and f0+f1=1 on a larger set t containing their union.
Русский
Если s0 и s1 компактны и не пересекаются, существуют функции с компактной поддержкой, неотрицательные, такие что f0=1 на s0, f1=1 на s1, и f0+f1=1 на надмножество t, содержащее их объединение.
LaTeX
$$$\\exists f_0,f_1\\in C_c(X,\\mathbb{R}_{\\ge0})\\, (f_0=1\\text{ on }s_0)\\land (f_1=1\\text{ on }s_1)\\land (f_0+f_1=1\\text{ on }t).$$$
Lean4
theorem exists_continuous_add_one_of_isCompact_nnreal {s₀ s₁ : Set X} {t : Set X} (s₀_compact : IsCompact s₀)
(s₁_compact : IsCompact s₁) (t_compact : IsCompact t) (disj : Disjoint s₀ s₁) (hst : s₀ ∪ s₁ ⊆ t) :
∃ (f₀ f₁ : C_c(X, ℝ≥0)), EqOn f₀ 1 s₀ ∧ EqOn f₁ 1 s₁ ∧ EqOn (f₀ + f₁) 1 t :=
by
set so : Fin 2 → Set X := fun j => if j = 0 then s₀ᶜ else s₁ᶜ with hso
have soopen (j : Fin 2) : IsOpen (so j) := by
fin_cases j
· simp only [hso, Fin.zero_eta, Fin.isValue, ↓reduceIte, isOpen_compl_iff]
exact IsCompact.isClosed <| s₀_compact
· simp only [hso, Fin.isValue, Fin.mk_one, one_ne_zero, ↓reduceIte, isOpen_compl_iff]
exact IsCompact.isClosed <| s₁_compact
have hsot : t ⊆ ⋃ j, so j := by
rw [hso]
simp only [Fin.isValue]
intro x hx
rw [mem_iUnion]
rw [← subset_compl_iff_disjoint_right, ← compl_compl s₀, compl_subset_iff_union] at disj
have h : x ∈ s₀ᶜ ∨ x ∈ s₁ᶜ := by
rw [← mem_union, disj]
exact mem_univ _
apply Or.elim h
· intro h0
use 0
simp only [Fin.isValue, ↓reduceIte]
exact h0
· intro h1
use 1
simp only [Fin.isValue, one_ne_zero, ↓reduceIte]
exact h1
obtain ⟨f, f_supp_in_so, sum_f_one_on_t, f_in_icc, f_hcs⟩ :=
exists_continuous_sum_one_of_isOpen_isCompact soopen t_compact hsot
use (nnrealPart (⟨f 1, f_hcs 1⟩ : C_c(X, ℝ))), (nnrealPart (⟨f 0, f_hcs 0⟩ : C_c(X, ℝ)))
simp only [Fin.isValue, CompactlySupportedContinuousMap.coe_add]
have sum_one_x (x : X) (hx : x ∈ t) : (f 0) x + (f 1) x = 1 := by
simpa only [Finset.sum_apply, Fin.sum_univ_two, Fin.isValue, Pi.one_apply] using sum_f_one_on_t hx
refine ⟨?_, ?_, ?_⟩
· intro x hx
simp only [Fin.isValue, nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk, Pi.one_apply,
Real.toNNReal_eq_one]
have : (f 0) x = 0 := by
rw [← notMem_support]
have : s₀ ⊆ (tsupport (f 0))ᶜ :=
by
apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 0))
rw [hso]
simp only [Fin.isValue, ↓reduceIte, compl_compl, subset_refl]
apply notMem_of_mem_compl
exact mem_of_subset_of_mem (subset_trans this (compl_subset_compl_of_subset subset_closure)) hx
rw [union_subset_iff] at hst
rw [← sum_one_x x (mem_of_subset_of_mem hst.1 hx), this]
exact Eq.symm (AddZeroClass.zero_add ((f 1) x))
· intro x hx
simp only [Fin.isValue, nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk, Pi.one_apply,
Real.toNNReal_eq_one]
have : (f 1) x = 0 := by
rw [← notMem_support]
have : s₁ ⊆ (tsupport (f 1))ᶜ :=
by
apply subset_trans _ (compl_subset_compl.mpr (f_supp_in_so 1))
rw [hso]
simp only [Fin.isValue, one_ne_zero, ↓reduceIte, compl_compl, subset_refl]
apply notMem_of_mem_compl
exact mem_of_subset_of_mem (subset_trans this (compl_subset_compl_of_subset subset_closure)) hx
rw [union_subset_iff] at hst
rw [← sum_one_x x (mem_of_subset_of_mem hst.2 hx), this]
exact Eq.symm (AddMonoid.add_zero ((f 0) x))
· intro x hx
simp only [Fin.isValue, Pi.add_apply, nnrealPart_apply, CompactlySupportedContinuousMap.coe_mk, Pi.one_apply]
rw [Real.toNNReal_add_toNNReal (f_in_icc 1 x).1 (f_in_icc 0 x).1, add_comm]
simp only [Fin.isValue, Real.toNNReal_eq_one]
exact sum_one_x x hx
