English
Dualizing the previous result yields countability for the set of x with z < f(x) and monotone constraints on f within t.
Русский
Дублируя предыдущее утверждение, получаем счётность для множества x с z < f(x) и монотонными ограничениями на f внутри t.
LaTeX
$$countable ({x ∈ t | ∃ z, z < f x ∧ ∀ y ∈ t, 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. -/
theorem countable_image_gt_image_Ioi [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
Set.Countable {x | ∃ z, z < f x ∧ ∀ y, x < y → f y ≤ z} :=
countable_image_lt_image_Ioi (α := αᵒᵈ) f