English
For any ideal I in C(X,𝕜), the ideal generated by setOfIdeal(I) via idealOfSet equals the closure of I.
Русский
Для идеала I в C(X,𝕜) идеал, порожденный setOfIdeal(I), равен замыканию I.
LaTeX
$$$ idealOfSet(𝕜, setOfIdeal(I)) = \\overline{I} $$$
Lean4
/-- An auxiliary lemma used in the proof of `ContinuousMap.idealOfSet_ofIdeal_eq_closure` which may
be useful on its own. -/
theorem exists_mul_le_one_eqOn_ge (f : C(X, ℝ≥0)) {c : ℝ≥0} (hc : 0 < c) :
∃ g : C(X, ℝ≥0), (∀ x : X, (g * f) x ≤ 1) ∧ {x : X | c ≤ f x}.EqOn (g * f) 1 :=
⟨{ toFun := (f ⊔ const X c)⁻¹
continuous_toFun := ((map_continuous f).sup <| map_continuous _).inv₀ fun _ => (hc.trans_le le_sup_right).ne' },
fun x => (inv_mul_le_iff₀ (hc.trans_le le_sup_right)).mpr ((mul_one (f x ⊔ c)).symm ▸ le_sup_left), fun x hx => by
simpa only [coe_const, mul_apply, coe_mk, Pi.inv_apply, Pi.sup_apply, Function.const_apply,
sup_eq_left.mpr (Set.mem_setOf.mp hx), ne_eq, Pi.one_apply] using inv_mul_cancel₀ (hc.trans_le hx).ne'⟩
