ProCGroups/InverseSystems/Utilities.lean
1import Mathlib.Topology.Homeomorph.Lemmas
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/InverseSystems/Utilities.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Inverse systems and inverse limits
14Defines inverse systems of topological groups and proves lift, projection, exactness, quotient, stagewise isomorphism, and finite-stage factorization results.
15-/
17namespace Continuous
19/-- A continuous bijection from a compact space to a Hausdorff space is a homeomorphism. -/
20noncomputable def homeoOfBijectiveCompactToT2
21 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
22 [CompactSpace X] [T2Space Y] {f : X → Y} (hf : Continuous f)
23 (hbij : Function.Bijective f) :
24 X ≃ₜ Y :=
25 homeoOfEquivCompactToT2 (f := Equiv.ofBijective f hbij) hf
27end Continuous
29namespace ProCGroups.InverseSystems
31universe u
33section
35variable {I : Type u} [Preorder I]
37/-- A finite subset of a directed preorder admits an upper bound. -/
38theorem exists_upperBound_finset (hdir : Directed (· ≤ ·) (id : I → I)) :
39 ∀ s : Finset I, s.Nonempty → ∃ j, ∀ i ∈ s, i ≤ j := by
40 classical
41 intro s
42 refine Finset.induction_on s ?_ ?_
43 · intro hs
44 rcases hs with ⟨i, hi⟩
45 simp only [Finset.notMem_empty] at hi
46 · intro a s ha ih hs
47 by_cases hs' : s.Nonempty
48 · rcases ih hs' with ⟨j, hj⟩
49 rcases hdir a j with ⟨k, hak, hjk⟩
50 refine ⟨k, ?_⟩
51 intro i hi
52 rw [Finset.mem_insert] at hi
53 rcases hi with rfl | hi
54 · exact hak
55 · exact (hj i hi).trans hjk
56 · have hs'' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs'
57 subst hs''
58 refine ⟨a, ?_⟩
59 intro i hi
60 simp only [insert_empty_eq, Finset.mem_singleton] at hi
61 simp only [hi, le_refl]
63end
65end ProCGroups.InverseSystems