Theorems · Theorem · general topology

countable_image_gt_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, ∀ y ∈ t, x < y → f y ≤ z}.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 below from f x is countable. We give here a version relative to a set t.

Defined in

Mathlib.Topology.Order.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderTopologyLinearOrderSecondCountableTopology