Shrinking open sets into dense open sets of finite products

The open unit cube in a finite product of copies of ℝ is open.

Given nonempty open sets V i in a topological space X and a dense open set U ⊆ κ → X for a finite type κ, the sets V i can be shrunk to nonempty open subsets so that the box ∏ j, W (t j) along one given injective tuple t : κ → I lies in U. When the index type I is also finite, iterating this shrinks the V i so that, for finitely many dense open sets U c ⊆ κ c → X with each κ c finite, every box along every injective tuple t : κ c → I lies in U c. Such shrinking steps are the basic move in Baire category constructions of perfect sets of independent points, such as the proof of Mycielski's theorem.

In a Hausdorff space the injective tuples indexed by a finite type form an open subset of the product, such as the ordered triples of distinct points of the Riemann sphere.

Main results

• TauCeti.isOpen_setOf_forall_abs_lt_one: the finite-dimensional open unit cube is open.
• TauCeti.exists_univ_pi_subset: shrinking along one injective tuple.
• TauCeti.exists_forall_univ_pi_subset: when the index type is finite, shrinking along all injective tuples for finitely many dense open sets at once.
• TauCeti.isOpen_setOf_injective: in a Hausdorff space, the injective finite tuples form an open set.

theorem TauCeti.isOpen_setOf_forall_abs_lt_one {ι : Type u_1} [Finite ι] : IsOpen {z : ι → ℝ | ∀ (i : ι), |z i| < 1}

The open unit cube in a finite product of copies of ℝ is open.

theorem TauCeti.isOpen_setOf_injective {X : Type u_1} [TopologicalSpace X] [T2Space X] {κ : Type u_2} [Finite κ] : IsOpen {t : κ → X | Function.Injective t}

In a Hausdorff space, the injective tuples indexed by a finite type form an open subset of the product: injectivity asks finitely many pairs of coordinates to differ.

theorem TauCeti.exists_univ_pi_subset {X : Type u_1} [TopologicalSpace X] {I : Type u_2} {κ : Type u_3} [Finite κ] {V : I → Set X} (hVo : ∀ (i : I), IsOpen (V i)) (hVne : ∀ (i : I), (V i).Nonempty) {t : κ → I} (ht : Function.Injective t) {U : Set (κ → X)} (hUo : IsOpen U) (hUd : Dense U) : ∃ (W : I → Set X), (∀ (i : I), IsOpen (W i)) ∧ (∀ (i : I), (W i).Nonempty) ∧ (∀ (i : I), W i ⊆ V i) ∧ (Set.univ.pi fun (j : κ) => W (t j)) ⊆ U

Shrinking along one injective tuple: nonempty open sets V i can be shrunk to nonempty open sets W i ⊆ V i so that the box ∏ j, W (t j) along an injective finite tuple t of indices lies in a given dense open set. This is the inductive step of exists_forall_univ_pi_subset.

theorem TauCeti.exists_forall_univ_pi_subset {X : Type u_1} [TopologicalSpace X] {I : Type u_2} {C : Type u_3} [Finite I] [Finite C] {κ : C → Type u_4} [∀ (c : C), Finite (κ c)] {V : I → Set X} (hVo : ∀ (i : I), IsOpen (V i)) (hVne : ∀ (i : I), (V i).Nonempty) {U : (c : C) → Set (κ c → X)} (hUo : ∀ (c : C), IsOpen (U c)) (hUd : ∀ (c : C), Dense (U c)) : ∃ (W : I → Set X), (∀ (i : I), IsOpen (W i)) ∧ (∀ (i : I), (W i).Nonempty) ∧ (∀ (i : I), W i ⊆ V i) ∧ ∀ (c : C) (t : κ c → I), Function.Injective t → (Set.univ.pi fun (j : κ c) => W (t j)) ⊆ U c

Shrinking along all injective tuples. Nonempty open sets V i, indexed by a finite type, can be shrunk to nonempty open sets W i ⊆ V i so that for each of finitely many dense open sets U c ⊆ κ c → X, every box ∏ j, W (t j) along an injective tuple t : κ c → I lies in U c.

theorem TauCeti.not_discreteTopology_pi {ι : Type u_2} {Y : ι → Type u_3} [(i : ι) → TopologicalSpace (Y i)] [Infinite ι] [∀ (i : ι), Nontrivial (Y i)] : ¬DiscreteTopology ((i : ι) → Y i)

An infinite product of nontrivial spaces is not discrete: every basic open set constrains only finitely many coordinates, so it contains a point differing from any given one in a free coordinate.