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)
: