From 5c105c89bd6c50c7476dec67004ca65afc82638d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matias=20Heikkil=C3=A4?= Date: Fri, 15 Apr 2022 19:54:15 +0300 Subject: [PATCH] unique_stone_cech_extend --- src/topology/stone_cech.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/topology/stone_cech.lean b/src/topology/stone_cech.lean index 497e64c4b8734..9703b5b9588b3 100644 --- a/src/topology/stone_cech.lean +++ b/src/topology/stone_cech.lean @@ -262,6 +262,20 @@ ultrafilter_extend_extends f lemma continuous_stone_cech_extend : continuous (stone_cech_extend hf) := continuous_quot_lift _ (continuous_ultrafilter_extend f) +lemma unique_stone_cech_extend {g: stone_cech α → γ} (hg: continuous g) +(hfg: g ∘ stone_cech_unit = (stone_cech_extend hf) ∘ stone_cech_unit): +g = stone_cech_extend hf := +begin + have h_eq_on: eq_on g (stone_cech_extend hf) (range stone_cech_unit) := + begin + rw eq_on, + rintros _ ⟨a, ha⟩, + rw [← ha, ← function.comp_apply g stone_cech_unit a], + rw [← function.comp_apply (stone_cech_extend hf) stone_cech_unit a, hfg], + end, + exact continuous.ext_on dense_range_stone_cech_unit hg (continuous_stone_cech_extend hf) h_eq_on, +end + end extension lemma convergent_eqv_pure {u : ultrafilter α} {x : α} (ux : ↑u ≤ 𝓝 x) : u ≈ pure x :=