mathlib3 documentation

mathlib-counterexamples / sorgenfrey_line

Sorgenfrey line #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define sorgenfrey_line (notation: ℝₗ) to be the Sorgenfrey line. It is the real line with the topology space structure generated by half-open intervals set.Ico a b.

We prove that this line is a completely normal Hausdorff space but its product with itself is not a normal space. In particular, this implies that the topology on ℝₗ is neither metrizable, nor second countable.

Notations #

ℝₗ: Sorgenfrey line.

TODO #

Prove that the Sorgenfrey line is a paracompact space.

@[protected, instance]

noncomputable def counterexample.sorgenfrey_line.linear_ordered_field :

linear_ordered_field counterexample.sorgenfrey_line

@[protected, instance]

def counterexample.sorgenfrey_line.archimedean :

archimedean counterexample.sorgenfrey_line

@[protected, instance]

noncomputable def counterexample.sorgenfrey_line.conditionally_complete_linear_order :

conditionally_complete_linear_order counterexample.sorgenfrey_line

def counterexample.sorgenfrey_line :

The Sorgenfrey line. It is the real line with the topology space structure generated by half-open intervals set.Ico a b.

Equations

counterexample.sorgenfrey_line = ℝ

Instances for counterexample.sorgenfrey_line

noncomputable def counterexample.sorgenfrey_line.to_real :

counterexample.sorgenfrey_line ≃+* ℝ

Ring homomorphism between the Sorgenfrey line and the standard real line.

Equations

counterexample.sorgenfrey_line.to_real = ring_equiv.refl ℝ

@[protected, instance]

def counterexample.sorgenfrey_line.topological_space :

topological_space counterexample.sorgenfrey_line

Equations

counterexample.sorgenfrey_line.topological_space = topological_space.generate_from {s : set counterexample.sorgenfrey_line | ∃ (a b : counterexample.sorgenfrey_line), set.Ico a b = s}

theorem counterexample.sorgenfrey_line.is_open_Ico (a b : counterexample.sorgenfrey_line) :

is_open (set.Ico a b)

theorem counterexample.sorgenfrey_line.is_open_Ici (a : counterexample.sorgenfrey_line) :

is_open (set.Ici a)

theorem counterexample.sorgenfrey_line.nhds_basis_Ico (a : counterexample.sorgenfrey_line) :

(nhds a).has_basis (λ (b : counterexample.sorgenfrey_line), a < b) (λ (b : counterexample.sorgenfrey_line), set.Ico a b)

theorem counterexample.sorgenfrey_line.nhds_basis_Ico_rat (a : counterexample.sorgenfrey_line) :

(nhds a).has_countable_basis (λ (r : ℚ), a < ↑r) (λ (r : ℚ), set.Ico a ↑r)

theorem counterexample.sorgenfrey_line.nhds_basis_Ico_inv_pnat (a : counterexample.sorgenfrey_line) :

(nhds a).has_basis (λ (n : ℕ+), true) (λ (n : ℕ+), set.Ico a (a + (↑n)⁻¹))

theorem counterexample.sorgenfrey_line.nhds_countable_basis_Ico_inv_pnat (a : counterexample.sorgenfrey_line) :

(nhds a).has_countable_basis (λ (n : ℕ+), true) (λ (n : ℕ+), set.Ico a (a + (↑n)⁻¹))

theorem counterexample.sorgenfrey_line.nhds_antitone_basis_Ico_inv_pnat (a : counterexample.sorgenfrey_line) :

(nhds a).has_antitone_basis (λ (n : ℕ+), set.Ico a (a + (↑n)⁻¹))

theorem counterexample.sorgenfrey_line.is_open_iff {s : set counterexample.sorgenfrey_line} :

is_open s ↔ ∀ (x : counterexample.sorgenfrey_line), x ∈ s → (∃ (y : counterexample.sorgenfrey_line) (H : y > x), set.Ico x y ⊆ s)

theorem counterexample.sorgenfrey_line.is_closed_iff {s : set counterexample.sorgenfrey_line} :

is_closed s ↔ ∀ (x : counterexample.sorgenfrey_line), x ∉ s → (∃ (y : counterexample.sorgenfrey_line) (H : y > x), disjoint (set.Ico x y) s)

theorem counterexample.sorgenfrey_line.exists_Ico_disjoint_closed {a : counterexample.sorgenfrey_line} {s : set counterexample.sorgenfrey_line} (hs : is_closed s) (ha : a ∉ s) :

∃ (b : counterexample.sorgenfrey_line) (H : b > a), disjoint (set.Ico a b) s

@[simp]

theorem counterexample.sorgenfrey_line.map_to_real_nhds (a : counterexample.sorgenfrey_line) :

filter.map ⇑counterexample.sorgenfrey_line.to_real (nhds a) = nhds_within (⇑counterexample.sorgenfrey_line.to_real a) (set.Ici (⇑counterexample.sorgenfrey_line.to_real a))

theorem counterexample.sorgenfrey_line.nhds_eq_map (a : counterexample.sorgenfrey_line) :

nhds a = filter.map ⇑(counterexample.sorgenfrey_line.to_real.symm) (nhds_within (⇑counterexample.sorgenfrey_line.to_real a) (set.Ici (⇑counterexample.sorgenfrey_line.to_real a)))

theorem counterexample.sorgenfrey_line.nhds_eq_comap (a : counterexample.sorgenfrey_line) :

nhds a = filter.comap ⇑counterexample.sorgenfrey_line.to_real (nhds_within (⇑counterexample.sorgenfrey_line.to_real a) (set.Ici (⇑counterexample.sorgenfrey_line.to_real a)))

@[continuity]

theorem counterexample.sorgenfrey_line.continuous_to_real :

continuous ⇑counterexample.sorgenfrey_line.to_real

@[protected, instance]

def counterexample.sorgenfrey_line.order_closed_topology :

order_closed_topology counterexample.sorgenfrey_line

@[protected, instance]

def counterexample.sorgenfrey_line.has_continuous_add :

has_continuous_add counterexample.sorgenfrey_line

theorem counterexample.sorgenfrey_line.is_clopen_Ici (a : counterexample.sorgenfrey_line) :

is_clopen (set.Ici a)

theorem counterexample.sorgenfrey_line.is_clopen_Iio (a : counterexample.sorgenfrey_line) :

is_clopen (set.Iio a)

theorem counterexample.sorgenfrey_line.is_clopen_Ico (a b : counterexample.sorgenfrey_line) :

is_clopen (set.Ico a b)

@[protected, instance]

def counterexample.sorgenfrey_line.totally_disconnected_space :

totally_disconnected_space counterexample.sorgenfrey_line

@[protected, instance]

def counterexample.sorgenfrey_line.topological_space.first_countable_topology :

topological_space.first_countable_topology counterexample.sorgenfrey_line

@[protected, instance]

def counterexample.sorgenfrey_line.t5_space :

t5_space counterexample.sorgenfrey_line

Sorgenfrey line is a completely normal Hausdorff topological space.

theorem counterexample.sorgenfrey_line.dense_range_coe_rat :

dense_range coe

@[protected, instance]

def counterexample.sorgenfrey_line.topological_space.separable_space :

topological_space.separable_space counterexample.sorgenfrey_line

theorem counterexample.sorgenfrey_line.is_closed_antidiagonal (c : counterexample.sorgenfrey_line) :

is_closed {x : counterexample.sorgenfrey_line × counterexample.sorgenfrey_line | x.fst + x.snd = c}

theorem counterexample.sorgenfrey_line.is_clopen_Ici_prod (x : counterexample.sorgenfrey_line × counterexample.sorgenfrey_line) :

is_clopen (set.Ici x)

theorem counterexample.sorgenfrey_line.is_closed_of_subset_antidiagonal {s : set (counterexample.sorgenfrey_line × counterexample.sorgenfrey_line)} {c : counterexample.sorgenfrey_line} (hs : ∀ (x : counterexample.sorgenfrey_line × counterexample.sorgenfrey_line), x ∈ s → x.fst + x.snd = c) :

Any subset of an antidiagonal {(x, y) : ℝₗ × ℝₗ| x + y = c} is a closed set.

theorem counterexample.sorgenfrey_line.nhds_prod_antitone_basis_inv_pnat (x y : counterexample.sorgenfrey_line) :

(nhds (x, y)).has_antitone_basis (λ (n : ℕ+), set.Ico x (x + (↑n)⁻¹) ×ˢ set.Ico y (y + (↑n)⁻¹))

theorem counterexample.sorgenfrey_line.not_normal_space_prod :

¬normal_space (counterexample.sorgenfrey_line × counterexample.sorgenfrey_line)

The product of the Sorgenfrey line and itself is not a normal topological space.

theorem counterexample.sorgenfrey_line.not_metrizable_space :

¬topological_space.metrizable_space counterexample.sorgenfrey_line

Topology on the Sorgenfrey line is not metrizable.

theorem counterexample.sorgenfrey_line.not_second_countable_topology :

¬topological_space.second_countable_topology counterexample.sorgenfrey_line

Topology on the Sorgenfrey line is not second countable.