English
Within a second-countable ordered space, the set of x with f(x) separated to the right is countable.
Русский
В пространстве с порядком, второй счетностью, множество x с отделением справа счётно.
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_Iio_within [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β)
(f : β → α) : Set.Countable ({x ∈ t | ∃ z, f x < z ∧ ∀ y ∈ t, y < x → z ≤ f y}) :=
countable_image_lt_image_Ioi_within (β := βᵒᵈ) t f