Theorems · Theorem · general topology

countable_image_lt_image_Ioi_within

∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α),
  {x | x ∈ t ∧ ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}.Countable

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.

Defined in

Mathlib.Topology.Order.Basic

Cited by

3 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceLinearOrderOrderTopologyLinearOrderSecondCountableTopology