countable_image_gt_image_Iio_within

English

Within a second-countable ordered space, the set of x with left-sided separation by some z is countable.

Русский

В пространстве с порядком и счетностью левая сепарация задаёт множество счётное.

LaTeX

$$countable ({x ∈ t | ∃ z, z < f x ∧ ∀ y ∈ t, y < x → 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_Iio_within [OrderTopology α] [LinearOrder β] [SecondCountableTopology α] (t : Set β)
    (f : β → α) : Set.Countable ({x ∈ t | ∃ z, z < f x ∧ ∀ y ∈ t, y < x → f y ≤ z}) :=
  countable_image_lt_image_Ioi_within (α := αᵒᵈ) (β := βᵒᵈ) t f

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