Countably many infinite intervals separate points #
In this file we prove that in a linear order with second countable order topology,
the points can be separated by countably many infinite intervals.
We prove 4 versions of this statement (one for each of the infinite intervals),
as well as provide convenience corollaries about Filter.EventuallyEq.
instance HasCountableSeparatingOn.range_Iio {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {s : Set X} :
HasCountableSeparatingOn X (fun (x : Set X) => x ∈ Set.range Set.Iio) s
instance HasCountableSeparatingOn.range_Ioi {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {s : Set X} :
HasCountableSeparatingOn X (fun (x : Set X) => x ∈ Set.range Set.Ioi) s
instance HasCountableSeparatingOn.range_Iic {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {s : Set X} :
HasCountableSeparatingOn X (fun (x : Set X) => x ∈ Set.range Set.Iic) s
instance HasCountableSeparatingOn.range_Ici {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {s : Set X} :
HasCountableSeparatingOn X (fun (x : Set X) => x ∈ Set.range Set.Ici) s
theorem Filter.EventuallyEq.of_forall_eventually_lt_iff {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X} (h : ∀ (x : X), ∀ᶠ (a : α) in l, f a < x ↔ g a < x) :
theorem Filter.EventuallyEq.of_forall_eventually_le_iff {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X} (h : ∀ (x : X), ∀ᶠ (a : α) in l, f a ≤ x ↔ g a ≤ x) :
theorem Filter.EventuallyEq.of_forall_eventually_gt_iff {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X} (h : ∀ (x : X), ∀ᶠ (a : α) in l, x < f a ↔ x < g a) :
theorem Filter.EventuallyEq.of_forall_eventually_ge_iff {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] [SecondCountableTopology X] {α : Type u_2} {l : Filter α} [CountableInterFilter l] {f g : α → X} (h : ∀ (x : X), ∀ᶠ (a : α) in l, x ≤ f a ↔ x ≤ g a) :