countable_image_gt_image_Iio — Mathlib

English

A variant counting set of x in t with f x separated above by z inside t under second countability.

Русский

Вариант счётности множества x внутри t с отделением сверху z.

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

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