English
For a 𝕜 with RCLike structure, under suitable compactness and T2 assumptions, the equality setOfIdeal(idealOfSet 𝕜 s) = interior(s) holds.
Русский
При допустимой структуре 𝕜 и условиях компактности и T2 выполняется равенство setOfIdeal(idealOfSet 𝕜 s) = interior(s).
LaTeX
$$$ setOfIdeal(idealOfSet(𝕜, s)) = \\operatorname{int}(s) $$$
Lean4
@[simp]
theorem setOfIdeal_ofSet_eq_interior (s : Set X) : setOfIdeal (idealOfSet 𝕜 s) = interior s :=
by
refine
Set.Subset.antisymm
((setOfIdeal_open (idealOfSet 𝕜 s)).subset_interior_iff.mpr fun x hx =>
let ⟨f, hf, hfx⟩ := mem_setOfIdeal.mp hx
Set.notMem_compl_iff.mp (mt (@hf x) hfx))
fun x hx =>
?_
-- If `x ∉ closure sᶜ`, we must produce `f : C(X, 𝕜)` which is zero on `sᶜ` and `f x ≠ 0`.
rw [← compl_compl (interior s), ← closure_compl] at hx
simp_rw [mem_setOfIdeal, mem_idealOfSet]
/- Apply Urysohn's lemma to get `g : C(X, ℝ)` which is zero on `sᶜ` and `g x ≠ 0`, then compose
with the natural embedding `ℝ ↪ 𝕜` to produce the desired `f`. -/
obtain ⟨g, hgs, hgx : Set.EqOn g 1 { x }, -⟩ :=
exists_continuous_zero_one_of_isClosed isClosed_closure isClosed_singleton (Set.disjoint_singleton_right.mpr hx)
exact
⟨⟨fun x => g x, continuous_ofReal.comp (map_continuous g)⟩, by
simpa only [coe_mk, ofReal_eq_zero] using fun x hx => hgs (subset_closure hx), by
simpa only [coe_mk, hgx (Set.mem_singleton x), Pi.one_apply, RCLike.ofReal_one] using one_ne_zero⟩
