English
The family of sets of the form x ∈ range Iio provides a countable separating family on s.
Русский
Семейство множеств вида x ∈ range Iio образует счётное разделяющее семейство на s.
LaTeX
$$$ HasCountableSeparatingOn X (\cdot \in range Iio) s $$$
Lean4
instance range_Iio : HasCountableSeparatingOn X (· ∈ range Iio) s :=
by
constructor
rcases TopologicalSpace.exists_countable_dense X with ⟨s, hsc, hsd⟩
set t := s ∪ {x | ∃ y, y ⋖ x}
refine ⟨Iio '' t, .image ?_ _, ?_, ?_⟩
· exact hsc.union countable_setOf_covBy_left
· exact image_subset_range _ _
· rintro x - y - h
by_contra! hne
wlog hlt : x < y generalizing x y
· refine this y x ?_ hne.symm (hne.lt_or_gt.resolve_left hlt)
simpa only [iff_comm] using h
cases (Ioo x y).eq_empty_or_nonempty with
| inl he =>
specialize h (Iio y) (mem_image_of_mem _ (.inr ⟨x, hlt, by simpa using Set.ext_iff.mp he⟩))
simp [hlt.not_ge] at h
| inr hne =>
rcases hsd.inter_open_nonempty _ isOpen_Ioo hne with ⟨z, ⟨hxz, hzy⟩, hzs⟩
simpa [hxz, hzy.not_gt] using h (Iio z) (mem_image_of_mem _ (.inl hzs))
