Topology on ω-sequences

The topology on ω-sequences is essentially the product topology when ωSequence α is viewed as the product space Π (n : ℕ), α, where α is equipped with the discrete topology. The notion of "cylinders" are also ported from Π (n : ℕ), α and they form a topological basis.

@[instance_reducible]

instance Cslib.ωSequence.instTopologicalSpace {α : Type u_1} : TopologicalSpace (ωSequence α)

Define the topology on ωSequence α using an equivalence from it to the product topology ℕ → WithDiscreteTopology α.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.ωSequence.homeomorph {α : Type u_1} : ωSequence α ≃ₜ (ℕ → WithDiscreteTopology α)

The homeomorphisim from ωSequence α to ℕ → WithDiscreteTopology α.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cslib.ωSequence.homeomorph_apply {α : Type u_1} (xs : ωSequence α) (i : ℕ) : homeomorph xs i = WithTopology.toTopology ⊥ (xs i)

@[simp]

theorem Cslib.ωSequence.homeomorph_symm_apply {α : Type u_1} (f : ℕ → WithDiscreteTopology α) : homeomorph.symm f = { get := fun (i : ℕ) => (f i).ofTopology }

def Cslib.ωSequence.cylinder {α : Type u_1} (xs : ωSequence α) (n : ℕ) : Set (ωSequence α)

Port the notion of "cylinders" from ℕ → WithDiscreteTopology α to ωSequence α.

Equations

• xs.cylinder n = ⇑Cslib.ωSequence.homeomorph ⁻¹' PiNat.cylinder (Cslib.ωSequence.homeomorph xs) n

theorem Cslib.ωSequence.cylinder_def {α : Type u_1} (xs : ωSequence α) (n : ℕ) : xs.cylinder n = {ys : ωSequence α | ∀ k < n, ys k = xs k}

An alternative characterization of cylinders in terms of ωSequence α alone.

theorem Cslib.ωSequence.cylinder_eq_prepend_range {α : Type u_1} (xs : ωSequence α) (n : ℕ) : xs.cylinder n = Set.range fun (x : ωSequence α) => take n xs ++ω x

Yet another alternative characterization of cylinders in terms of ωSequence α alone.

theorem Cslib.ωSequence.isTopologicalBasis_cylinders {α : Type u_1} : TopologicalSpace.IsTopologicalBasis {s : Set (ωSequence α) | ∃ (xs : ωSequence α) (n : ℕ), s = xs.cylinder n}

The cylinders form a topological basis.

theorem Cslib.ωSequence.isOpen_cylinder {α : Type u_1} (xs : ωSequence α) (n : ℕ) : IsOpen (xs.cylinder n)

All cylinders are open sets.

theorem Cslib.ωSequence.nhds_cylinders {α : Type u_1} {xs : ωSequence α} {s : Set (ωSequence α)} (hx : xs ∈ s) (hs : IsOpen s) : ∃ (ys : ωSequence α) (n : ℕ), xs ∈ ys.cylinder n ∧ ys.cylinder n ⊆ s

Every ω-sequence in an open set belongs to a cylinder which is contained in the set.

theorem Cslib.ωSequence.isOpen_iff {α : Type u_1} (s : Set (ωSequence α)) : IsOpen s ↔ ∀ xs ∈ s, ∃ (n : ℕ), ∀ (ys : ωSequence α), take n xs ++ω ys ∈ s

A set is open iff any ω-sequence in the set has a finite prefix all of whose infinite extensions are also in the set.

theorem Cslib.ωSequence.dense_iff {α : Type u_1} (s : Set (ωSequence α)) : Dense s ↔ ∀ (xs : ωSequence α) (n : ℕ), ∃ (ys : ωSequence α), take n xs ++ω ys ∈ s

A set is dense iff any finite sequence can be extended to an infinite sequence in the set.