English
For a function taking values in a second-countable space, the set of points x ∈ t with f(x) separated below by some z is countable.
Русский
Для функции, принимающей значения во второй счетной пространстве, множество x ∈ t, для которых f(x) отделено снизу некоторым z, счётно.
LaTeX
$$countable ({x ∈ t | ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y})$$
Lean4
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated above from `f x` is countable. We give
here a version relative to a set `t`. -/
theorem countable_image_lt_image_Ioi_within [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β)
(f : β → α) : Set.Countable ({x ∈ t | ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}) := by
/- If the values of `f` are separated above on the right of `x`, there is an interval `(f x, z x)`
which is not reached by `f`. This gives a family of disjoint open intervals in `α`. Such a
family can only be countable as `α` is second-countable. -/
nontriviality β
have : Nonempty α := Nonempty.map f (by infer_instance)
let s := {x ∈ t | ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y := fun x hx ↦
hx.2
-- choose `z x` such that `f` does not take the values in `(f x, z x)`.
choose! z hz using this
have I : InjOn f s := by
apply StrictMonoOn.injOn
intro x hx y hy hxy
calc
f x < z x := (hz x hx).1
_ ≤ f y := (hz x hx).2 y hy.1 hxy
have fs_count : (f '' s).Countable :=
by
have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) :=
by
rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
wlog hle : u ≤ v generalizing u v
· exact (this v vs u us huv.symm (le_of_not_ge hle)).symm
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
apply disjoint_iff_forall_ne.2
rintro a ha b hb rfl
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)
apply Set.PairwiseDisjoint.countable_of_Ioo A
rintro _ ⟨y, ys, rfl⟩
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count
