mathlib3 documentation

topology.metric_space.pi_nat

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

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

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:

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

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

pi_nat.exists_retraction_of_is_closed: 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_complete_space: 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.

pi_countable.dist is the distance on Π i, E i given by dist x y = ∑' i, min (1/2)^(encode i) (dist (x i) (y i)).
pi_countable.metric_space is the corresponding metric space structure, adjusted so that the uniformity is definitionally the product uniformity. Not registered as an instance.

The first_diff function #

@[irreducible]

noncomputable def pi_nat.first_diff {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) :

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

Equations

pi_nat.first_diff x y = dite (x ≠ y) (λ (h : x ≠ y), nat.find _) (λ (h : ¬x ≠ y), 0)

theorem pi_nat.apply_first_diff_ne {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} (h : x ≠ y) :

x (pi_nat.first_diff x y) ≠ y (pi_nat.first_diff x y)

theorem pi_nat.apply_eq_of_lt_first_diff {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} {n : ℕ} (hn : n < pi_nat.first_diff x y) :

x n = y n

theorem pi_nat.first_diff_comm {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) :

pi_nat.first_diff x y = pi_nat.first_diff y x

theorem pi_nat.min_first_diff_le {E : ℕ → Type u_1} (x y z : Π (n : ℕ), E n) (h : x ≠ z) :

linear_order.min (pi_nat.first_diff x y) (pi_nat.first_diff y z) ≤ pi_nat.first_diff x z

Cylinders #

def pi_nat.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

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

theorem pi_nat.cylinder_eq_pi {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) (n : ℕ) :

pi_nat.cylinder x n = ↑(finset.range n).pi (λ (i : ℕ), {x i})

@[simp]

theorem pi_nat.cylinder_zero {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) :

pi_nat.cylinder x 0 = set.univ

theorem pi_nat.cylinder_anti {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) {m n : ℕ} (h : m ≤ n) :

pi_nat.cylinder x n ⊆ pi_nat.cylinder x m

@[simp]

theorem pi_nat.mem_cylinder_iff {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} {n : ℕ} :

y ∈ pi_nat.cylinder x n ↔ ∀ (i : ℕ), i < n → y i = x i

theorem pi_nat.self_mem_cylinder {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) (n : ℕ) :

x ∈ pi_nat.cylinder x n

theorem pi_nat.mem_cylinder_iff_eq {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} {n : ℕ} :

y ∈ pi_nat.cylinder x n ↔ pi_nat.cylinder y n = pi_nat.cylinder x n

theorem pi_nat.mem_cylinder_comm {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) (n : ℕ) :

y ∈ pi_nat.cylinder x n ↔ x ∈ pi_nat.cylinder y n

theorem pi_nat.mem_cylinder_iff_le_first_diff {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} (hne : x ≠ y) (i : ℕ) :

x ∈ pi_nat.cylinder y i ↔ i ≤ pi_nat.first_diff x y

theorem pi_nat.mem_cylinder_first_diff {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) :

x ∈ pi_nat.cylinder y (pi_nat.first_diff x y)

theorem pi_nat.cylinder_eq_cylinder_of_le_first_diff {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) {n : ℕ} (hn : n ≤ pi_nat.first_diff x y) :

pi_nat.cylinder x n = pi_nat.cylinder y n

theorem pi_nat.Union_cylinder_update {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) (n : ℕ) :

(⋃ (k : E n), pi_nat.cylinder (function.update x n k) (n + 1)) = pi_nat.cylinder x n

theorem pi_nat.update_mem_cylinder {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) (n : ℕ) (y : E n) :

function.update x n y ∈ pi_nat.cylinder x n

def pi_nat.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

pi_nat.res x n.succ = x n :: pi_nat.res x n
pi_nat.res x 0 = list.nil

@[simp]

theorem pi_nat.res_zero {α : Type u_2} (x : ℕ → α) :

pi_nat.res x 0 = list.nil

@[simp]

theorem pi_nat.res_succ {α : Type u_2} (x : ℕ → α) (n : ℕ) :

pi_nat.res x n.succ = x n :: pi_nat.res x n

@[simp]

theorem pi_nat.res_length {α : Type u_2} (x : ℕ → α) (n : ℕ) :

(pi_nat.res x n).length = n

theorem pi_nat.res_eq_res {α : Type u_2} {x y : ℕ → α} {n : ℕ} :

pi_nat.res x n = pi_nat.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 pi_nat.res_injective {α : Type u_2} :

function.injective pi_nat.res

theorem pi_nat.cylinder_eq_res {α : Type u_2} (x : ℕ → α) (n : ℕ) :

pi_nat.cylinder x n = {y : ℕ → α | pi_nat.res y n = pi_nat.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 has_dist instance nor a metric_spaceinstance, as other distances may be used on these spaces, but we register them as local instances in this section.

@[protected]

noncomputable def pi_nat.has_dist {E : ℕ → Type u_1} :

has_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

pi_nat.has_dist = {dist := λ (x y : Π (n : ℕ), E n), dite (x ≠ y) (λ (h : x ≠ y), (1 / 2) ^ pi_nat.first_diff x y) (λ (h : ¬x ≠ y), 0)}

theorem pi_nat.dist_eq_of_ne {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} (h : x ≠ y) :

has_dist.dist x y = (1 / 2) ^ pi_nat.first_diff x y

@[protected]

theorem pi_nat.dist_self {E : ℕ → Type u_1} (x : Π (n : ℕ), E n) :

has_dist.dist x x = 0

@[protected]

theorem pi_nat.dist_comm {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) :

has_dist.dist x y = has_dist.dist y x

@[protected]

theorem pi_nat.dist_nonneg {E : ℕ → Type u_1} (x y : Π (n : ℕ), E n) :

0 ≤ has_dist.dist x y

theorem pi_nat.dist_triangle_nonarch {E : ℕ → Type u_1} (x y z : Π (n : ℕ), E n) :

has_dist.dist x z ≤ linear_order.max (has_dist.dist x y) (has_dist.dist y z)

@[protected]

theorem pi_nat.dist_triangle {E : ℕ → Type u_1} (x y z : Π (n : ℕ), E n) :

has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z

@[protected]

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

x = y

theorem pi_nat.mem_cylinder_iff_dist_le {E : ℕ → Type u_1} {x y : Π (n : ℕ), E n} {n : ℕ} :

y ∈ pi_nat.cylinder x n ↔ has_dist.dist y x ≤ (1 / 2) ^ n

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

x i = y i

theorem pi_nat.lipschitz_with_one_iff_forall_dist_image_le_of_mem_cylinder {E : ℕ → Type u_1} {α : Type u_2} [pseudo_metric_space α] {f : (Π (n : ℕ), E n) → α} :

(∀ (x y : Π (n : ℕ), E n), has_dist.dist (f x) (f y) ≤ has_dist.dist x y) ↔ ∀ (x y : Π (n : ℕ), E n) (n : ℕ), y ∈ pi_nat.cylinder x n → has_dist.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 lipschitz_with as we don't have a metric space structure

theorem pi_nat.is_open_cylinder (E : ℕ → Type u_1) [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] (x : Π (n : ℕ), E n) (n : ℕ) :

is_open (pi_nat.cylinder x n)

theorem pi_nat.is_topological_basis_cylinders (E : ℕ → Type u_1) [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] :

topological_space.is_topological_basis {s : set (Π (n : ℕ), E n) | ∃ (x : Π (n : ℕ), E n) (n : ℕ), s = pi_nat.cylinder x n}

theorem pi_nat.is_open_iff_dist {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] (s : set (Π (n : ℕ), E n)) :

is_open s ↔ ∀ (x : Π (n : ℕ), E n), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : Π (n : ℕ), E n), has_dist.dist x y < ε → y ∈ s)

@[protected]

noncomputable def pi_nat.metric_space {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] :

metric_space (Π (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 metric_space_of_discrete_uniformity instead.

Equations

pi_nat.metric_space = metric_space.of_dist_topology has_dist.dist pi_nat.metric_space._proof_1 pi_nat.metric_space._proof_2 pi_nat.metric_space._proof_3 pi_nat.metric_space._proof_4 pi_nat.metric_space._proof_5

@[protected]

noncomputable def pi_nat.metric_space_of_discrete_uniformity {E : ℕ → Type u_1} [Π (n : ℕ), uniform_space (E n)] (h : ∀ (n : ℕ), uniformity (E n) = filter.principal id_rel) :

metric_space (Π (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

pi_nat.metric_space_of_discrete_uniformity h = {to_pseudo_metric_space := {to_has_dist := pi_nat.has_dist (λ (n : ℕ), E n), dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : Π (n : ℕ), E n), ↑⟨(λ (x y : Π (n : ℕ), (λ (n : ℕ), E n) n), dite (x ≠ y) (λ (h : x ≠ y), (1 / 2) ^ pi_nat.first_diff x y) (λ (h : ¬x ≠ y), 0)) x y, _⟩, edist_dist := _, to_uniform_space := Pi.uniform_space (λ (n : ℕ), E n) (λ (i : ℕ), _inst_3 i), uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : Π (n : ℕ), (λ (n : ℕ), E n) n), dite (x ≠ y) (λ (h : x ≠ y), (1 / 2) ^ pi_nat.first_diff x y) (λ (h : ¬x ≠ y), 0)) pi_nat.metric_space_of_discrete_uniformity._proof_7 pi_nat.metric_space_of_discrete_uniformity._proof_8 pi_nat.metric_space_of_discrete_uniformity._proof_9, cobounded_sets := _}, eq_of_dist_eq_zero := _}

noncomputable def pi_nat.metric_space_nat_nat :

metric_space (ℕ → ℕ)

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

pi_nat.metric_space_nat_nat = pi_nat.metric_space_of_discrete_uniformity pi_nat.metric_space_nat_nat._proof_1

@[protected]

theorem pi_nat.complete_space {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] :

complete_space (Π (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 pi_nat.exists_disjoint_cylinder {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) {x : Π (n : ℕ), E n} (hx : x ∉ s) :

∃ (n : ℕ), disjoint s (pi_nat.cylinder x n)

noncomputable def pi_nat.shortest_prefix_diff {E : ℕ → Type u_1} (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 shortest_prefix_diff 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

pi_nat.shortest_prefix_diff x s = dite (∃ (n : ℕ), disjoint s (pi_nat.cylinder x n)) (λ (h : ∃ (n : ℕ), disjoint s (pi_nat.cylinder x n)), nat.find h) (λ (h : ¬∃ (n : ℕ), disjoint s (pi_nat.cylinder x n)), 0)

theorem pi_nat.first_diff_lt_shortest_prefix_diff {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) {x y : Π (n : ℕ), E n} (hx : x ∉ s) (hy : y ∈ s) :

pi_nat.first_diff x y < pi_nat.shortest_prefix_diff x s

theorem pi_nat.shortest_prefix_diff_pos {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) (hne : s.nonempty) {x : Π (n : ℕ), E n} (hx : x ∉ s) :

0 < pi_nat.shortest_prefix_diff x s

noncomputable def pi_nat.longest_prefix {E : ℕ → Type u_1} (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 longest_prefix 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

pi_nat.longest_prefix x s = pi_nat.shortest_prefix_diff x s - 1

theorem pi_nat.first_diff_le_longest_prefix {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) {x y : Π (n : ℕ), E n} (hx : x ∉ s) (hy : y ∈ s) :

pi_nat.first_diff x y ≤ pi_nat.longest_prefix x s

theorem pi_nat.inter_cylinder_longest_prefix_nonempty {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) (hne : s.nonempty) (x : Π (n : ℕ), E n) :

(s ∩ pi_nat.cylinder x (pi_nat.longest_prefix x s)).nonempty

theorem pi_nat.disjoint_cylinder_of_longest_prefix_lt {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) {x : Π (n : ℕ), E n} (hx : x ∉ s) {n : ℕ} (hn : pi_nat.longest_prefix x s < n) :

disjoint s (pi_nat.cylinder x n)

theorem pi_nat.cylinder_longest_prefix_eq_of_longest_prefix_lt_first_diff {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {x y : Π (n : ℕ), E n} {s : set (Π (n : ℕ), E n)} (hs : is_closed s) (hne : s.nonempty) (H : pi_nat.longest_prefix x s < pi_nat.first_diff x y) (xs : x ∉ s) (ys : y ∉ s) :

pi_nat.cylinder x (pi_nat.longest_prefix x s) = pi_nat.cylinder y (pi_nat.longest_prefix 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 pi_nat.exists_lipschitz_retraction_of_is_closed {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) (hne : s.nonempty) :

∃ (f : (Π (n : ℕ), E n) → Π (n : ℕ), E n), (∀ (x : Π (n : ℕ), E n), x ∈ s → f x = x) ∧ set.range f = s ∧ lipschitz_with 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 pi_nat.exists_retraction_of_is_closed {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed s) (hne : s.nonempty) :

∃ (f : (Π (n : ℕ), E n) → Π (n : ℕ), E n), (∀ (x : Π (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 pi_nat.exists_retraction_subtype_of_is_closed {E : ℕ → Type u_1} [Π (n : ℕ), topological_space (E n)] [∀ (n : ℕ), discrete_topology (E n)] {s : set (Π (n : ℕ), E n)} (hs : is_closed 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_complete_space (α : Type u_1) [metric_space α] [complete_space α] [topological_space.second_countable_topology α] [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_polish_space.

Products of (possibly non-discrete) metric spaces #

@[protected]

noncomputable def pi_countable.has_dist {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] :

has_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

pi_countable.has_dist = {dist := λ (x y : Π (i : ι), F i), ∑' (i : ι), linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i))}

theorem pi_countable.dist_eq_tsum {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] (x y : Π (i : ι), F i) :

has_dist.dist x y = ∑' (i : ι), linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i))

theorem pi_countable.dist_summable {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] (x y : Π (i : ι), F i) :

summable (λ (i : ι), linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i)))

theorem pi_countable.min_dist_le_dist_pi {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] (x y : Π (i : ι), F i) (i : ι) :

linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i)) ≤ has_dist.dist x y

theorem pi_countable.dist_le_dist_pi_of_dist_lt {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] {x y : Π (i : ι), F i} {i : ι} (h : has_dist.dist x y < (1 / 2) ^ encodable.encode i) :

has_dist.dist (x i) (y i) ≤ has_dist.dist x y

@[protected]

noncomputable def pi_countable.metric_space {ι : Type u_2} [encodable ι] {F : ι → Type u_3} [Π (i : ι), metric_space (F i)] :

metric_space (Π (i : ι), F i)

Given a countable family of metric spaces, one may put a distance on their product Π i, E i, defining the right topology and uniform structure. It is highly non-canonical, though, and therefore not registered as a global instance. The distance we use here is dist x y = ∑' n, min (1/2)^(encode i) (dist (x n) (y n)).

Equations

pi_countable.metric_space = {to_pseudo_metric_space := {to_has_dist := pi_countable.has_dist (λ (i : ι), _inst_2 i), dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : Π (i : ι), F i), ↑⟨(λ (x y : Π (i : ι), (λ (i : ι), F i) i), ∑' (i : ι), linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i))) x y, _⟩, edist_dist := _, to_uniform_space := Pi.uniform_space (λ (i : ι), F i) (λ (i : ι), pseudo_metric_space.to_uniform_space), uniformity_dist := _, to_bornology := bornology.of_dist (λ (x y : Π (i : ι), (λ (i : ι), F i) i), ∑' (i : ι), linear_order.min ((1 / 2) ^ encodable.encode i) (has_dist.dist (x i) (y i))) pi_countable.metric_space._proof_7 pi_countable.metric_space._proof_8 pi_countable.metric_space._proof_9, cobounded_sets := _}, eq_of_dist_eq_zero := _}