English
If i is a dense embedding with dense complement of its range, then any compact subset s of α has empty interior.
Русский
Если i — плотное вложение и дополнение образа плотное, то любой компактный подмножество α имеет пустоеInterior.
LaTeX
$$$ [T2Space β] (di : IsDenseInducing i) (hd : Dense (range i)ᶜ) {s : Set α} (hs : IsCompact s) : interior s = \\emptyset $$$
Lean4
/-- If `i : α → β` is a dense embedding with dense complement of the range, then any compact set in
`α` has empty interior. -/
theorem interior_compact_eq_empty [T2Space β] (di : IsDenseInducing i) (hd : Dense (range i)ᶜ) {s : Set α}
(hs : IsCompact s) : interior s = ∅ :=
by
refine eq_empty_iff_forall_notMem.2 fun x hx => ?_
rw [mem_interior_iff_mem_nhds] at hx
have := di.closure_image_mem_nhds hx
rw [(hs.image di.continuous).isClosed.closure_eq] at this
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
exact hyi (image_subset_range _ _ hys)
