[Merged by Bors] - feat(topology/stone_cech): add stone_cech_hom_ext

[mapehe]

The universal property that characterises the Stone–Čech compactification of a topological space X is that any function from X to a compact Hausdorff space extends uniquely to a continuous function on βX. Existence is already provided by unique_stone_cech_extend, but it seems that the uniqueness lemma was intentionally omitted previously. Easy, but probably worth being explicit about.

---

[adamtopaz]

Suggested change

	(hfg: g ∘ stone_cech_unit = (stone_cech_extend hf) ∘ stone_cech_unit):
	g = stone_cech_extend hf :=
	(hfg: g ∘ stone_cech_unit = (stone_cech_extend hf) ∘ stone_cech_unit) :
	g = stone_cech_extend hf :=

Just some minor spacing issues

[mapehe]

Is there an autoformatter for lean btw?

[adamtopaz]

Is there an autoformatter for lean btw?

I don't know! That would be useful indeed!

[adamtopaz]

The following lemma may be slightly more useful:

lemma stone_cech_hom_ext {g₁ g₂ : stone_cech α → γ} 
  (h₁ : continuous g₁) (h₂ : continuous g₂) 
  (h : g₁ ∘ stone_cech_unit = g₂ ∘ stone_cech_unit) : g₁ = g₂ :=
begin
  apply continuous.ext_on dense_range_stone_cech_unit h₁ h₂,
  rintros x ⟨x, rfl⟩,
  apply (congr_fun h x)
end

[mapehe]

Thanks @adamtopaz, agreed that your formulation is more useful and commited your suggestion. 🙏

[adamtopaz]

LGTM! I'll wait to see if there are any other comments, and for CI to finish before merging.
(It would be good to get another reviewer's comments, since I suggested the current formulation of the lemma.)

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

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