English
For a function into a second-countable space, the set of x with f(x) separated from above by some z is countable.
Русский
Для функции в пространство со второй счетностью множество x, где f(x) отделено сверху некоторым z, счётно.
LaTeX
$$countable ( {x | ∃ z, z < f x ∧ ∀ y ∈ domain, x < y → f y ≤ z} )$$
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 below from `f x` is countable. We give
here a version relative to a set `t`. -/
theorem countable_image_gt_image_Ioi_within [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β)
(f : β → α) : Set.Countable ({x ∈ t | ∃ z, z < f x ∧ ∀ y ∈ t, x < y → f y ≤ z}) :=
countable_image_lt_image_Ioi_within (α := αᵒᵈ) t f
