countable_image_lt_image_Iio_within

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

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