countable_image_gt_image_Ioi — Mathlib

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

Похожие утверждения