Topological study of spaces Π (n : ℕ), E n

When E n are topological spaces, the space Π (n : ℕ), E n is naturally a topological space (with the product topology). When E n are uniform spaces, it also inherits a uniform structure. However, it does not inherit a canonical metric space structure of the E n. Nevertheless, one can put a noncanonical metric space structure (or rather, several of them). This is done in this file.

Main definitions and results

One can define a combinatorial distance on Π (n : ℕ), E n, as follows:

• PiNat.cylinder x n is the set of points y with x i = y i for i < n.
• PiNat.firstDiff x y is the first index at which x i ≠ y i.
• PiNat.dist x y is equal to (1/2) ^ (firstDiff x y). It defines a distance on Π (n : ℕ), E n, compatible with the topology when the E n have the discrete topology.
• PiNat.metricSpace: the metric space structure, given by this distance. Not registered as an instance. This space is a complete metric space.
• PiNat.metricSpaceOfDiscreteUniformity: the same metric space structure, but adjusting the uniformity defeqness when the E n already have the discrete uniformity. Not registered as an instance
• PiNat.metricSpaceNatNat: the particular case of ℕ → ℕ, not registered as an instance.

These results are used to construct continuous functions on Π n, E n:

• PiNat.exists_retraction_of_isClosed: given a nonempty closed subset s of Π (n : ℕ), E n, there exists a retraction onto s, i.e., a continuous map from the whole space to s restricting to the identity on s.
• exists_nat_nat_continuous_surjective_of_completeSpace: given any nonempty complete metric space with second-countable topology, there exists a continuous surjection from ℕ → ℕ onto this space.

One can also put distances on Π (i : ι), E i when the spaces E i are metric spaces (not discrete in general), and ι is countable.

• PiCountable.dist is the distance on Π i, E i given by dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).
• PiCountable.metricSpace is the corresponding metric space structure, adjusted so that the uniformity is definitionally the product uniformity. Not registered as an instance.
• PiNatEmbed gives an equivalence between a space and itself in a sequence of spaces
• Metric.PiNatEmbed.metricSpace proves that a topological X separated by countably many continuous functions to metric spaces, can be embedded inside their product.

The firstDiff function

@[irreducible]

def PiNat.firstDiff {E : ℕ → Type u_2} (x y : (n : ℕ) → E n) : ℕ

In a product space Π n, E n, then firstDiff x y is the first index at which x and y differ. If x = y, then by convention we set firstDiff x x = 0.

Equations

• PiNat.firstDiff x y = if h : x ≠ y then Nat.find ⋯ else 0

theorem PiNat.firstDiff_def {E : ℕ → Type u_2} (x y : (n : ℕ) → E n) : firstDiff x y = if h : x ≠ y then Nat.find ⋯ else 0

theorem PiNat.apply_firstDiff_ne {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} (h : x ≠ y) : x (firstDiff x y) ≠ y (firstDiff x y)

theorem PiNat.apply_eq_of_lt_firstDiff {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ} (hn : n < firstDiff x y) : x n = y n

theorem PiNat.firstDiff_comm {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) : firstDiff x y = firstDiff y x

theorem PiNat.min_firstDiff_le {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n) (h : x ≠ z) : min (firstDiff x y) (firstDiff y z) ≤ firstDiff x z

Cylinders

def PiNat.cylinder {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) : Set ((n : ℕ) → E n)

In a product space Π n, E n, the cylinder set of length n around x, denoted cylinder x n, is the set of sequences y that coincide with x on the first n symbols, i.e., such that y i = x i for all i < n.

Equations

• PiNat.cylinder x n = {y : (n : ℕ) → E n | ∀ i < n, y i = x i}

theorem PiNat.cylinder_eq_pi {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) : cylinder x n = (↑(Finset.range n)).pi fun (i : ℕ) => {x i}

@[simp]

theorem PiNat.cylinder_zero {E : ℕ → Type u_1} (x : (n : ℕ) → E n) : cylinder x 0 = Set.univ

theorem PiNat.cylinder_anti {E : ℕ → Type u_1} (x : (n : ℕ) → E n) {m n : ℕ} (h : m ≤ n) : cylinder x n ⊆ cylinder x m

@[simp]

theorem PiNat.mem_cylinder_iff {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ} : y ∈ cylinder x n ↔ ∀ i < n, y i = x i

theorem PiNat.self_mem_cylinder {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) : x ∈ cylinder x n

theorem PiNat.mem_cylinder_iff_eq {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ} : y ∈ cylinder x n ↔ cylinder y n = cylinder x n

theorem PiNat.mem_cylinder_comm {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) (n : ℕ) : y ∈ cylinder x n ↔ x ∈ cylinder y n

theorem PiNat.mem_cylinder_iff_le_firstDiff {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} (hne : x ≠ y) (i : ℕ) : x ∈ cylinder y i ↔ i ≤ firstDiff x y

theorem PiNat.mem_cylinder_firstDiff {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) : x ∈ cylinder y (firstDiff x y)

theorem PiNat.cylinder_eq_cylinder_of_le_firstDiff {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) {n : ℕ} (hn : n ≤ firstDiff x y) : cylinder x n = cylinder y n

theorem PiNat.iUnion_cylinder_update {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) : ⋃ (k : E n), cylinder (Function.update x n k) (n + 1) = cylinder x n

theorem PiNat.update_mem_cylinder {E : ℕ → Type u_1} (x : (n : ℕ) → E n) (n : ℕ) (y : E n) : Function.update x n y ∈ cylinder x n

def PiNat.res {α : Type u_2} (x : ℕ → α) : ℕ → List α

In the case where E has constant value α, the cylinder cylinder x n can be identified with the element of List α consisting of the first n entries of x. See cylinder_eq_res. We call this list res x n, the restriction of x to n.

Equations

• PiNat.res x 0 = []
• PiNat.res x n.succ = x n :: PiNat.res x n

@[simp]

theorem PiNat.res_zero {α : Type u_2} (x : ℕ → α) : res x 0 = []

@[simp]

theorem PiNat.res_succ {α : Type u_2} (x : ℕ → α) (n : ℕ) : res x n.succ = x n :: res x n

@[simp]

theorem PiNat.res_length {α : Type u_2} (x : ℕ → α) (n : ℕ) : (res x n).length = n

theorem PiNat.res_eq_res {α : Type u_2} {x y : ℕ → α} {n : ℕ} : res x n = res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m

The restrictions of x and y to n are equal if and only if x m = y m for all m < n.

theorem PiNat.res_injective {α : Type u_2} : Function.Injective res

theorem PiNat.cylinder_eq_res {α : Type u_2} (x : ℕ → α) (n : ℕ) : cylinder x n = {y : ℕ → α | res y n = res x n}

cylinder x n is equal to the set of sequences y with the same restriction to n as x.

A distance function on Π n, E n

We define a distance function on Π n, E n, given by dist x y = (1/2)^n where n is the first index at which x and y differ. When each E n has the discrete topology, this distance will define the right topology on the product space. We do not record a global Dist instance nor a MetricSpace instance, as other distances may be used on these spaces, but we register them as local instances in this section.

def PiNat.dist {E : ℕ → Type u_1} : Dist ((n : ℕ) → E n)

The distance function on a product space Π n, E n, given by dist x y = (1/2)^n where n is the first index at which x and y differ.

Equations

• PiNat.dist = { dist := fun (x y : (n : ℕ) → E n) => if x ≠ y then (1 / 2) ^ PiNat.firstDiff x y else 0 }

theorem PiNat.dist_eq_of_ne {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} (h : x ≠ y) : dist x y = (1 / 2) ^ firstDiff x y

theorem PiNat.dist_self {E : ℕ → Type u_1} (x : (n : ℕ) → E n) : dist x x = 0

theorem PiNat.dist_comm {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) : dist x y = dist y x

theorem PiNat.dist_nonneg {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) : 0 ≤ dist x y

theorem PiNat.dist_triangle_nonarch {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n) : dist x z ≤ max (dist x y) (dist y z)

theorem PiNat.dist_triangle {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n) : dist x z ≤ dist x y + dist y z

theorem PiNat.eq_of_dist_eq_zero {E : ℕ → Type u_1} (x y : (n : ℕ) → E n) (hxy : dist x y = 0) : x = y

theorem PiNat.mem_cylinder_iff_dist_le {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ} : y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

theorem PiNat.apply_eq_of_dist_lt {E : ℕ → Type u_1} {x y : (n : ℕ) → E n} {n : ℕ} (h : dist x y < (1 / 2) ^ n) {i : ℕ} (hi : i ≤ n) : x i = y i

theorem PiNat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder {E : ℕ → Type u_1} {α : Type u_2} [PseudoMetricSpace α] {f : ((n : ℕ) → E n) → α} : (∀ (x y : (n : ℕ) → E n), dist (f x) (f y) ≤ dist x y) ↔ ∀ (x y : (n : ℕ) → E n) (n : ℕ), y ∈ cylinder x n → dist (f x) (f y) ≤ (1 / 2) ^ n

A function to a pseudo-metric-space is 1-Lipschitz if and only if points in the same cylinder of length n are sent to points within distance (1/2)^n. Not expressed using LipschitzWith as we don't have a metric space structure

theorem PiNat.isOpen_cylinder (E : ℕ → Type u_1) [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] (x : (n : ℕ) → E n) (n : ℕ) : IsOpen (cylinder x n)

theorem PiNat.isTopologicalBasis_cylinders (E : ℕ → Type u_1) [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] : TopologicalSpace.IsTopologicalBasis {s : Set ((n : ℕ) → E n) | ∃ (x : (n : ℕ) → E n) (n : ℕ), s = cylinder x n}

theorem PiNat.isOpen_iff_dist {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] (s : Set ((n : ℕ) → E n)) : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s

def PiNat.metricSpace {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] : MetricSpace ((n : ℕ) → E n)

Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete topology, where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default. Warning: this definition makes sure that the topology is defeq to the original product topology, but it does not take care of a possible uniformity. If the E n have a uniform structure, then there will be two non-defeq uniform structures on Π n, E n, the product one and the one coming from the metric structure. In this case, use metricSpaceOfDiscreteUniformity instead.

Equations

• PiNat.metricSpace = MetricSpace.ofDistTopology dist ⋯ ⋯ ⋯ ⋯ ⋯

def PiNat.metricSpaceOfDiscreteUniformity {E : ℕ → Type u_2} [(n : ℕ) → UniformSpace (E n)] (h : ∀ (n : ℕ), uniformity (E n) = Filter.principal SetRel.id) : MetricSpace ((n : ℕ) → E n)

Metric space structure on Π (n : ℕ), E n when the spaces E n have the discrete uniformity, where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default.

Equations

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

def PiNat.metricSpaceNatNat : MetricSpace (ℕ → ℕ)

Metric space structure on ℕ → ℕ where the distance is given by dist x y = (1/2)^n, where n is the smallest index where x and y differ. Not registered as a global instance by default.

Equations

• PiNat.metricSpaceNatNat = PiNat.metricSpaceOfDiscreteUniformity PiNat.metricSpaceNatNat._proof_1

theorem PiNat.completeSpace {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] : CompleteSpace ((n : ℕ) → E n)

Retractions inside product spaces

We show that, in a space Π (n : ℕ), E n where each E n is discrete, there is a retraction on any closed nonempty subset s, i.e., a continuous map f from the whole space to s restricting to the identity on s. The map f is defined as follows. For x ∈ s, let f x = x. Otherwise, consider the longest prefix w that x shares with an element of s, and let f x = z_w where z_w is an element of s starting with w.

theorem PiNat.exists_disjoint_cylinder {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) {x : (n : ℕ) → E n} (hx : x ∉ s) : ∃ (n : ℕ), Disjoint s (cylinder x n)

def PiNat.shortestPrefixDiff {E : ℕ → Type u_2} (x : (n : ℕ) → E n) (s : Set ((n : ℕ) → E n)) : ℕ

Given a point x in a product space Π (n : ℕ), E n, and s a subset of this space, then shortestPrefixDiff x s if the smallest n for which there is no element of s having the same prefix of length n as x. If there is no such n, then use 0 by convention.

Equations

• PiNat.shortestPrefixDiff x s = if h : ∃ (n : ℕ), Disjoint s (PiNat.cylinder x n) then Nat.find h else 0

theorem PiNat.firstDiff_lt_shortestPrefixDiff {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) {x y : (n : ℕ) → E n} (hx : x ∉ s) (hy : y ∈ s) : firstDiff x y < shortestPrefixDiff x s

theorem PiNat.shortestPrefixDiff_pos {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) {x : (n : ℕ) → E n} (hx : x ∉ s) : 0 < shortestPrefixDiff x s

def PiNat.longestPrefix {E : ℕ → Type u_2} (x : (n : ℕ) → E n) (s : Set ((n : ℕ) → E n)) : ℕ

Given a point x in a product space Π (n : ℕ), E n, and s a subset of this space, then longestPrefix x s if the largest n for which there is an element of s having the same prefix of length n as x. If there is no such n, use 0 by convention.

Equations

• PiNat.longestPrefix x s = PiNat.shortestPrefixDiff x s - 1

theorem PiNat.firstDiff_le_longestPrefix {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) {x y : (n : ℕ) → E n} (hx : x ∉ s) (hy : y ∈ s) : firstDiff x y ≤ longestPrefix x s

theorem PiNat.inter_cylinder_longestPrefix_nonempty {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) (x : (n : ℕ) → E n) : (s ∩ cylinder x (longestPrefix x s)).Nonempty

theorem PiNat.disjoint_cylinder_of_longestPrefix_lt {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) {x : (n : ℕ) → E n} (hx : x ∉ s) {n : ℕ} (hn : longestPrefix x s < n) : Disjoint s (cylinder x n)

theorem PiNat.cylinder_longestPrefix_eq_of_longestPrefix_lt_firstDiff {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {x y : (n : ℕ) → E n} {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) (H : longestPrefix x s < firstDiff x y) (xs : x ∉ s) (ys : y ∉ s) : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

If two points x, y coincide up to length n, and the longest common prefix of x with s is strictly shorter than n, then the longest common prefix of y with s is the same, and both cylinders of this length based at x and y coincide.

theorem PiNat.exists_lipschitz_retraction_of_isClosed {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) : ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n), (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ LipschitzWith 1 f

Given a closed nonempty subset s of Π (n : ℕ), E n, there exists a Lipschitz retraction onto this set, i.e., a Lipschitz map with range equal to s, equal to the identity on s.

theorem PiNat.exists_retraction_of_isClosed {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) : ∃ (f : ((n : ℕ) → E n) → (n : ℕ) → E n), (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ Continuous f

Given a closed nonempty subset s of Π (n : ℕ), E n, there exists a retraction onto this set, i.e., a continuous map with range equal to s, equal to the identity on s.

theorem PiNat.exists_retraction_subtype_of_isClosed {E : ℕ → Type u_1} [(n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)] {s : Set ((n : ℕ) → E n)} (hs : IsClosed s) (hne : s.Nonempty) : ∃ (f : ((n : ℕ) → E n) → ↑s), (∀ (x : ↑s), f ↑x = x) ∧ Function.Surjective f ∧ Continuous f

theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type u_2) [MetricSpace α] [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] : ∃ (f : (ℕ → ℕ) → α), Continuous f ∧ Function.Surjective f

Any nonempty complete second countable metric space is the continuous image of the fundamental space ℕ → ℕ. For a version of this theorem in the context of Polish spaces, see exists_nat_nat_continuous_surjective_of_polishSpace.

Products of (possibly non-discrete) metric spaces

def PiCountable.edist {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] : EDist ((i : ι) → F i)

Given a countable family of extended metric spaces, one may put an extended distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i)).

Equations

• PiCountable.edist = { edist := fun (x y : (i : ι) → F i) => ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (edist (x i) (y i)) }

theorem PiCountable.edist_eq_tsum {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] (x y : (i : ι) → F i) : edist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (edist (x i) (y i))

theorem PiCountable.min_edist_le_edist_pi {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] (x y : (i : ι) → F i) (i : ι) : min (2⁻¹ ^ Encodable.encode i) (edist (x i) (y i)) ≤ edist x y

theorem PiCountable.edist_le_two {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] {x y : (i : ι) → F i} : edist x y ≤ 2

theorem PiCountable.edist_lt_top {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] {x y : (i : ι) → F i} : edist x y < ⊤

theorem PiCountable.edist_le_edist_pi_of_edist_lt {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EDist (F i)] {x y : (i : ι) → F i} {i : ι} (h : edist x y < 2⁻¹ ^ Encodable.encode i) : edist (x i) (y i) ≤ edist x y

def PiCountable.pseudoEMetricSpace {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoEMetricSpace (F i)] : PseudoEMetricSpace ((i : ι) → F i)

Given a countable family of extended pseudo metric spaces, one may put an extended distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i)).

Equations

• PiCountable.pseudoEMetricSpace = { toEDist := PiCountable.edist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := Pi.uniformSpace F, uniformity_edist := ⋯ }

def PiCountable.emetricSpace {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → EMetricSpace (F i)] : EMetricSpace ((i : ι) → F i)

Given a countable family of extended metric spaces, one may put an extended distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i)).

Equations

• PiCountable.emetricSpace = { toPseudoEMetricSpace := PiCountable.pseudoEMetricSpace, eq_of_edist_eq_zero := ⋯ }

def PiCountable.dist {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] : Dist ((i : ι) → F i)

Given a countable family of metric spaces, one may put a distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).

Equations

• PiCountable.dist = { dist := fun (x y : (i : ι) → F i) => ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i)) }

theorem PiCountable.dist_eq_tsum {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] (x y : (i : ι) → F i) : dist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i))

theorem PiCountable.dist_summable {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] (x y : (i : ι) → F i) : Summable fun (i : ι) => min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i))

theorem PiCountable.min_dist_le_dist_pi {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] (x y : (i : ι) → F i) (i : ι) : min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i)) ≤ dist x y

theorem PiCountable.dist_le_dist_pi_of_dist_lt {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] {x y : (i : ι) → F i} {i : ι} (h : dist x y < 2⁻¹ ^ Encodable.encode i) : dist (x i) (y i) ≤ dist x y

def PiCountable.pseudoMetricSpace {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → PseudoMetricSpace (F i)] : PseudoMetricSpace ((i : ι) → F i)

Given a countable family of metric spaces, one may put a distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).

Equations

• PiCountable.pseudoMetricSpace = PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯

def PiCountable.metricSpace {ι : Type u_2} [Encodable ι] {F : ι → Type u_3} [(i : ι) → MetricSpace (F i)] : MetricSpace ((i : ι) → F i)

Given a countable family of metric spaces, one may put a distance on their product Π i, E i.

It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`.

Equations

• PiCountable.metricSpace = EMetricSpace.toMetricSpaceOfDist dist ⋯ ⋯

Embedding a countably separated space inside a space of sequences

structure Metric.PiNatEmbed {ι : Type u_2} (X : Type u_5) (Y : ι → Type u_6) (f : (i : ι) → X → Y i) : Type u_5

Given a type X and a sequence Y of metric spaces and a sequence f : : ∀ i, X → Y i of separating functions, PiNatEmbed X Y f is a type synonym for X seen as a subset of ∀ i, Y i.

• toPiNat :: (
• ofPiNat : X

  The map from the subset of ∀ i, Y i to X.

• )

theorem Metric.PiNatEmbed.ext {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : PiNatEmbed X Y f} (hxy : x.ofPiNat = y.ofPiNat) : x = y

theorem Metric.PiNatEmbed.ext_iff {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : PiNatEmbed X Y f} : x = y ↔ x.ofPiNat = y.ofPiNat

def Metric.PiNatEmbed.toPiNatEquiv {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) : X ≃ PiNatEmbed X Y f

Equivalence between X and its embedding into ∀ i, Y i.

Equations

• Metric.PiNatEmbed.toPiNatEquiv X Y f = { toFun := Metric.PiNatEmbed.toPiNat, invFun := Metric.PiNatEmbed.ofPiNat, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Metric.PiNatEmbed.toPiNatEquiv_symm_apply {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) (self : PiNatEmbed X Y f) : (toPiNatEquiv X Y f).symm self = self.ofPiNat

@[simp]

theorem Metric.PiNatEmbed.toPiNatEquiv_apply_ofPiNat {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) (ofPiNat : X) : ((toPiNatEquiv X Y f) ofPiNat).ofPiNat = ofPiNat

@[simp]

theorem Metric.PiNatEmbed.ofPiNat_inj {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {x y : PiNatEmbed X Y f} : x.ofPiNat = y.ofPiNat ↔ x = y

@[simp]

theorem Metric.PiNatEmbed.forall {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {P : PiNatEmbed X Y f → Prop} : (∀ (x : PiNatEmbed X Y f), P x) ↔ ∀ (x : X), P { ofPiNat := x }

noncomputable def Metric.PiNatEmbed.embed {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) : PiNatEmbed X Y f → (i : ι) → Y i

X equipped with the distance coming from ∀ i, Y i embeds in ∀ i, Y i.

Equations

• Metric.PiNatEmbed.embed X Y f x i = f i x.ofPiNat

theorem Metric.PiNatEmbed.embed_injective {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : Function.Injective (embed X Y f)

noncomputable instance Metric.PiNatEmbed.instPseudoEMetricSpace {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoEMetricSpace (Y i)] : PseudoEMetricSpace (PiNatEmbed X Y f)

Equations

• Metric.PiNatEmbed.instPseudoEMetricSpace = PseudoEMetricSpace.induced (Metric.PiNatEmbed.embed X Y f) PiCountable.pseudoEMetricSpace

theorem Metric.PiNatEmbed.edist_def {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoEMetricSpace (Y i)] (x y : PiNatEmbed X Y f) : edist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (edist (f i x.ofPiNat) (f i y.ofPiNat))

theorem Metric.PiNatEmbed.isometry_embed {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoEMetricSpace (Y i)] : Isometry (embed X Y f)

noncomputable instance Metric.PiNatEmbed.instPseudoMetricSpace {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoMetricSpace (Y i)] : PseudoMetricSpace (PiNatEmbed X Y f)

Equations

• Metric.PiNatEmbed.instPseudoMetricSpace = PseudoMetricSpace.induced (Metric.PiNatEmbed.embed X Y f) PiCountable.pseudoMetricSpace

theorem Metric.PiNatEmbed.dist_def {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoMetricSpace (Y i)] (x y : PiNatEmbed X Y f) : dist x y = ∑' (i : ι), min (2⁻¹ ^ Encodable.encode i) (dist (f i x.ofPiNat) (f i y.ofPiNat))

theorem Metric.PiNatEmbed.continuous_toPiNat {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → PseudoMetricSpace (Y i)] [TopologicalSpace X] (continuous_f : ∀ (i : ι), Continuous (f i)) : Continuous toPiNat

@[reducible, inline]

noncomputable abbrev Metric.PiNatEmbed.emetricSpace {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → EMetricSpace (Y i)] (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : EMetricSpace (PiNatEmbed X Y f)

If the functions f i : X → Y i separate points of X, then X can be embedded into ∀ i, Y i.

Equations

• Metric.PiNatEmbed.emetricSpace separating_f = EMetricSpace.induced (Metric.PiNatEmbed.embed X Y f) ⋯ PiCountable.emetricSpace

theorem Metric.PiNatEmbed.isUniformEmbedding_embed {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → EMetricSpace (Y i)] (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : IsUniformEmbedding (embed X Y f)

@[reducible, inline]

noncomputable abbrev Metric.PiNatEmbed.metricSpace {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → MetricSpace (Y i)] (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : MetricSpace (PiNatEmbed X Y f)

If the functions f i : X → Y i separate points of X, then X can be embedded into ∀ i, Y i.

Equations

• Metric.PiNatEmbed.metricSpace separating_f = EMetricSpace.toMetricSpace ⋯

theorem Metric.PiNatEmbed.isHomeomorph_toPiNat {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} [Encodable ι] [(i : ι) → MetricSpace (Y i)] [TopologicalSpace X] [CompactSpace X] (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : IsHomeomorph toPiNat

noncomputable def Metric.PiNatEmbed.toPiNatHomeo {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) [Encodable ι] [(i : ι) → MetricSpace (Y i)] [TopologicalSpace X] [CompactSpace X] (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : X ≃ₜ PiNatEmbed X Y f

Homeomorphism between X and its embedding into ∀ i, Y i induced by a separating family of continuous functions f i : X → Y i.

Equations

• Metric.PiNatEmbed.toPiNatHomeo X Y f continuous_f separating_f = (Metric.PiNatEmbed.toPiNatEquiv X Y f).toHomeomorphOfIsInducing ⋯

@[simp]

theorem Metric.PiNatEmbed.toPiNatHomeo_apply_ofPiNat {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) [Encodable ι] [(i : ι) → MetricSpace (Y i)] [TopologicalSpace X] [CompactSpace X] (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) (ofPiNat : X) : ((toPiNatHomeo X Y f continuous_f separating_f) ofPiNat).ofPiNat = ofPiNat

@[simp]

theorem Metric.PiNatEmbed.toPiNatHomeo_symm_apply {ι : Type u_2} (X : Type u_3) (Y : ι → Type u_4) (f : (i : ι) → X → Y i) [Encodable ι] [(i : ι) → MetricSpace (Y i)] [TopologicalSpace X] [CompactSpace X] (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) (self : PiNatEmbed X Y f) : (toPiNatHomeo X Y f continuous_f separating_f).symm self = self.ofPiNat

theorem Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} [Encodable ι] [(i : ι) → MetricSpace (Y i)] [TopologicalSpace X] [CompactSpace X] (f : (i : ι) → X → Y i) (continuous_f : ∀ (i : ι), Continuous (f i)) (separating_f : Pairwise fun (x y : X) => ∃ (i : ι), f i x ≠ f i y) : TopologicalSpace.MetrizableSpace X

If X is compact, and there exists a sequence of continuous functions f i : X → Y i to metric spaces Y i that separate points on X, then X is metrizable.