English
For f1 ≤ f2 in CompactlySupportedContinuousMap α ℝ≥0, there exists g ∈ C_c(α, ℝ≥0) such that f1 + g = f2.
Русский
Для f1 ≤ f2 в C_c(α, ℝ≥0) существует g ∈ C_c(α, ℝ≥0) such that f1 + g = f2.
LaTeX
$$$$ f_1 \le f_2 \Rightarrow \exists g \in C_c(\alpha, \mathbb{R}_{\ge 0}),\ f_1 + g = f_2. $$$$
Lean4
protected theorem exists_add_of_le {f₁ f₂ : C_c(α, ℝ≥0)} (h : f₁ ≤ f₂) : ∃ (g : C_c(α, ℝ≥0)), f₁ + g = f₂ :=
by
refine ⟨⟨f₂.1 - f₁.1, ?_⟩, ?_⟩
· apply (f₁.hasCompactSupport'.union f₂.hasCompactSupport').of_isClosed_subset isClosed_closure
rw [tsupport, tsupport, ← closure_union]
apply closure_mono
intro x hx
contrapose! hx
simp only [ContinuousMap.toFun_eq_coe, coe_toContinuousMap, Set.mem_union, Function.mem_support, ne_eq, not_or,
Decidable.not_not, ContinuousMap.coe_sub, Pi.sub_apply] at hx ⊢
simp [hx.1, hx.2]
· ext x
simpa [← NNReal.coe_add] using add_tsub_cancel_of_le (h x)
