Sorgenfrey line

In this file we define SorgenfreyLine (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.

def Counterexample.SorgenfreyLine : Type

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

def SorgenfreyLine.termℝₗ : Lean.ParserDescr

instance Counterexample.instConditionallyCompleteLinearOrderSorgenfreyLine : ConditionallyCompleteLinearOrder Counterexample.SorgenfreyLine

instance Counterexample.instLinearOrderedFieldSorgenfreyLine : LinearOrderedField Counterexample.SorgenfreyLine

instance Counterexample.instArchimedeanSorgenfreyLineToOrderedAddCommMonoidToOrderedSemiringToOrderedCommSemiringToStrictOrderedCommSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstLinearOrderedFieldSorgenfreyLine : Archimedean Counterexample.SorgenfreyLine

def Counterexample.SorgenfreyLine.toReal : Counterexample.SorgenfreyLine ≃+* ℝ

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

instance Counterexample.SorgenfreyLine.instTopologicalSpaceSorgenfreyLine : TopologicalSpace Counterexample.SorgenfreyLine

theorem Counterexample.SorgenfreyLine.isOpen_Ico (a : Counterexample.SorgenfreyLine) (b : Counterexample.SorgenfreyLine) : IsOpen (Set.Ico a b)

theorem Counterexample.SorgenfreyLine.isOpen_Ici (a : Counterexample.SorgenfreyLine) : IsOpen (Set.Ici a)

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico (a : Counterexample.SorgenfreyLine) : Filter.HasBasis (nhds a) (fun x => a < x) fun x => Set.Ico a x

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_rat (a : Counterexample.SorgenfreyLine) : Filter.HasCountableBasis (nhds a) (fun r => a < ↑r) fun r => Set.Ico a ↑r

theorem Counterexample.SorgenfreyLine.nhds_basis_Ico_inv_pnat (a : Counterexample.SorgenfreyLine) : Filter.HasBasis (nhds a) (fun x => True) fun n => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.nhds_countable_basis_Ico_inv_pnat (a : Counterexample.SorgenfreyLine) : Filter.HasCountableBasis (nhds a) (fun x => True) fun n => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.nhds_antitone_basis_Ico_inv_pnat (a : Counterexample.SorgenfreyLine) : Filter.HasAntitoneBasis (nhds a) fun n => Set.Ico a (a + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.isOpen_iff {s : Set Counterexample.SorgenfreyLine} : IsOpen s ↔ ∀ (x : Counterexample.SorgenfreyLine), x ∈ s → ∃ y, y > x ∧ Set.Ico x y ⊆ s

theorem Counterexample.SorgenfreyLine.isClosed_iff {s : Set Counterexample.SorgenfreyLine} : IsClosed s ↔ ∀ (x : Counterexample.SorgenfreyLine), ¬x ∈ s → ∃ y, y > x ∧ Disjoint (Set.Ico x y) s

theorem Counterexample.SorgenfreyLine.exists_Ico_disjoint_closed {a : Counterexample.SorgenfreyLine} {s : Set Counterexample.SorgenfreyLine} (hs : IsClosed s) (ha : ¬a ∈ s) : ∃ b, b > a ∧ Disjoint (Set.Ico a b) s

@[simp]

theorem Counterexample.SorgenfreyLine.map_toReal_nhds (a : Counterexample.SorgenfreyLine) : Filter.map (↑Counterexample.SorgenfreyLine.toReal) (nhds a) = nhdsWithin (↑Counterexample.SorgenfreyLine.toReal a) (Set.Ici (↑Counterexample.SorgenfreyLine.toReal a))

theorem Counterexample.SorgenfreyLine.nhds_eq_map (a : Counterexample.SorgenfreyLine) : nhds a = Filter.map (↑(RingEquiv.symm Counterexample.SorgenfreyLine.toReal)) (nhdsWithin (↑Counterexample.SorgenfreyLine.toReal a) (Set.Ici (↑Counterexample.SorgenfreyLine.toReal a)))

theorem Counterexample.SorgenfreyLine.nhds_eq_comap (a : Counterexample.SorgenfreyLine) : nhds a = Filter.comap (↑Counterexample.SorgenfreyLine.toReal) (nhdsWithin (↑Counterexample.SorgenfreyLine.toReal a) (Set.Ici (↑Counterexample.SorgenfreyLine.toReal a)))

theorem Counterexample.SorgenfreyLine.continuous_toReal : Continuous ↑Counterexample.SorgenfreyLine.toReal

instance Counterexample.SorgenfreyLine.instOrderClosedTopologySorgenfreyLineInstTopologicalSpaceSorgenfreyLineToPreorderToPartialOrderToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingInstLinearOrderedFieldSorgenfreyLine : OrderClosedTopology Counterexample.SorgenfreyLine

instance Counterexample.SorgenfreyLine.instContinuousAddSorgenfreyLineInstTopologicalSpaceSorgenfreyLineToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingInstLinearOrderedFieldSorgenfreyLine : ContinuousAdd Counterexample.SorgenfreyLine

theorem Counterexample.SorgenfreyLine.isClopen_Ici (a : Counterexample.SorgenfreyLine) : IsClopen (Set.Ici a)

theorem Counterexample.SorgenfreyLine.isClopen_Iio (a : Counterexample.SorgenfreyLine) : IsClopen (Set.Iio a)

theorem Counterexample.SorgenfreyLine.isClopen_Ico (a : Counterexample.SorgenfreyLine) (b : Counterexample.SorgenfreyLine) : IsClopen (Set.Ico a b)

instance Counterexample.SorgenfreyLine.instTotallyDisconnectedSpaceSorgenfreyLineInstTopologicalSpaceSorgenfreyLine : TotallyDisconnectedSpace Counterexample.SorgenfreyLine

instance Counterexample.SorgenfreyLine.instFirstCountableTopologySorgenfreyLineInstTopologicalSpaceSorgenfreyLine : TopologicalSpace.FirstCountableTopology Counterexample.SorgenfreyLine

instance Counterexample.SorgenfreyLine.instT5SpaceSorgenfreyLineInstTopologicalSpaceSorgenfreyLine : T5Space Counterexample.SorgenfreyLine

Sorgenfrey line is a completely normal Hausdorff topological space.

theorem Counterexample.SorgenfreyLine.denseRange_coe_rat : DenseRange Rat.cast

instance Counterexample.SorgenfreyLine.instSeparableSpaceSorgenfreyLineInstTopologicalSpaceSorgenfreyLine : TopologicalSpace.SeparableSpace Counterexample.SorgenfreyLine

theorem Counterexample.SorgenfreyLine.isClosed_antidiagonal (c : Counterexample.SorgenfreyLine) : IsClosed {x | x.fst + x.snd = c}

theorem Counterexample.SorgenfreyLine.isClopen_Ici_prod (x : Counterexample.SorgenfreyLine × Counterexample.SorgenfreyLine) : IsClopen (Set.Ici x)

theorem Counterexample.SorgenfreyLine.cardinal_antidiagonal (c : Counterexample.SorgenfreyLine) : Cardinal.mk ↑{x | x.fst + x.snd = c} = Cardinal.continuum

theorem Counterexample.SorgenfreyLine.isClosed_of_subset_antidiagonal {s : Set (Counterexample.SorgenfreyLine × Counterexample.SorgenfreyLine)} {c : Counterexample.SorgenfreyLine} (hs : ∀ (x : Counterexample.SorgenfreyLine × Counterexample.SorgenfreyLine), x ∈ s → x.fst + x.snd = c) : IsClosed s

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

instance Counterexample.SorgenfreyLine.instDiscreteTopologyElemProdSorgenfreyLineSetOfEqHAddInstHAddToAddToDistribToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingToRingToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingInstLinearOrderedFieldSorgenfreyLineFstSndInstTopologicalSpaceSubtypeMemSetInstMembershipSetInstTopologicalSpaceProdInstTopologicalSpaceSorgenfreyLine (c : Counterexample.SorgenfreyLine) : DiscreteTopology ↑{x | x.fst + x.snd = c}

theorem Counterexample.SorgenfreyLine.not_normalSpace_prod : ¬NormalSpace (Counterexample.SorgenfreyLine × Counterexample.SorgenfreyLine)

The Sorgenfrey plane ℝₗ × ℝₗ is not a normal space.

theorem Counterexample.SorgenfreyLine.isSeparable_antidiagonal (c : Counterexample.SorgenfreyLine) : TopologicalSpace.IsSeparable {x | x.fst + x.snd = c}

An antidiagonal is a separable set but is not a separable space.

theorem Counterexample.SorgenfreyLine.not_separableSpace_antidiagonal (c : Counterexample.SorgenfreyLine) : ¬TopologicalSpace.SeparableSpace ↑{x | x.fst + x.snd = c}

An antidiagonal is a separable set but is not a separable space.

theorem Counterexample.SorgenfreyLine.nhds_prod_antitone_basis_inv_pnat (x : Counterexample.SorgenfreyLine) (y : Counterexample.SorgenfreyLine) : Filter.HasAntitoneBasis (nhds (x, y)) fun n => Set.Ico x (x + (↑↑n)⁻¹) ×ˢ Set.Ico y (y + (↑↑n)⁻¹)

theorem Counterexample.SorgenfreyLine.not_separatedNhds_rat_irrational_antidiag : ¬SeparatedNhds {x | x.fst + x.snd = 0 ∧ ∃ r, ↑r = x.fst} {x | x.fst + x.snd = 0 ∧ Irrational (↑Counterexample.SorgenfreyLine.toReal x.fst)}

The sets of rational and irrational points of the antidiagonal {(x, y) | x + y = 0} cannot be separated by open neighborhoods. This implies that ℝₗ × ℝₗ is not a normal space.

theorem Counterexample.SorgenfreyLine.not_metrizableSpace : ¬TopologicalSpace.MetrizableSpace Counterexample.SorgenfreyLine

Topology on the Sorgenfrey line is not metrizable.

theorem Counterexample.SorgenfreyLine.not_secondCountableTopology : ¬TopologicalSpace.SecondCountableTopology Counterexample.SorgenfreyLine

Topology on the Sorgenfrey line is not second countable.