[Merged by Bors] - feat(topology/continuous_function): Any T0 space embeds in a product of copies of the Sierpinski space

[isadofschi]

Any T0 space embeds in a product of copies of the Sierpinski space

---

• I'm not sure where this should go.

[kmill]

Would you mind writing this lemma in this way? I think it would be easier to maintain, and I for one find it easier to follow.

Suggested change

	lemma eq_induced_by_maps_to_sierpinski (X : Type*) [t : topological_space X] :
	t = ⨅ (u : opens X), topological_space.induced (λ x, x ∈ u) sierpinski_space :=
	le_antisymm
	(le_infi_iff.2 (λ u, continuous.le_induced $ is_open_iff_continuous_mem.1 u.2))
	(is_open_implies_is_open_iff.mp $ λ u h,
	begin
	apply is_open_implies_is_open_iff.mpr _ u _,
	{ exact topological_space.induced (λ (x : X), x ∈ u) sierpinski_space },
	{ exact infi_le_of_le ⟨u,h⟩ (le_refl _) },
	{ exact is_open_induced_iff'.mpr ⟨{true}, ⟨is_open_singleton_true, by simp [set.preimage]⟩⟩ },
	end)
	lemma eq_induced_by_maps_to_sierpinski (X : Type*) [t : topological_space X] :
	t = ⨅ (u : opens X), sierpinski_space.induced (∈ u) :=
	begin
	apply le_antisymm,
	{ rw [le_infi_iff],
	exact λ u, continuous.le_induced (is_open_iff_continuous_mem.mp u.2) },
	{ intros u h,
	rw ← generate_from_Union_is_open,
	apply is_open_generate_from_of_mem,
	simp only [set.mem_Union, set.mem_set_of_eq, is_open_induced_iff'],
	exact ⟨⟨u, h⟩, {true}, is_open_singleton_true, by simp [set.preimage]⟩ },
	end

You can write (λ x, x ∈ u) instead of (∈ u) if you want -- this is just a common way to write the predicate.

This depends on the following missing lemma (it should go in topology/sets/opens.lean before or after mem_coe):

@[simp] lemma topological_space.opens.mem_mk {x : α} {U : set α} {h : is_open U} :
  @has_mem.mem _ _ opens.has_mem x ⟨U, h⟩ ↔ x ∈ U := iff.rfl

[kmill]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests