countable_image_lt_image_Ioi — Mathlib

English

In a second-countable order topology, the set of x ∈ t with x to the left of f is countable when considered within t.

Русский

Во второй счетной топологии порядка множество x ∈ t таких, что существует разделение слева от f, счётно.

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 above from `f x` is countable. -/
theorem countable_image_lt_image_Ioi [OrderTopology α] [LinearOrder β] (f : β → α) [SecondCountableTopology α] :
    Set.Countable {x | ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y} := by simpa using countable_image_lt_image_Ioi_within univ f

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