Source: ProCGroups.InverseSystems.Utilities
1import Mathlib.Topology.Homeomorph.Lemmas
3/-!
4# Order-theoretic utilities for inverse systems
6The finite-upper-bound lemma in this module turns directedness of a preorder into a single stage
7dominating any nonempty finite set of indices. It is the common combinatorial step in
8compactness, cofinality, and finite-coordinate arguments for inverse limits.
9-/
11namespace ProCGroups.InverseSystems
13universe u
15section
17variable {I : Type u} [Preorder I]
19/-- A finite subset of a directed preorder admits an upper bound. -/
20theorem exists_upperBound_finset (hdir : Directed (· ≤ ·) (id : I → I)) :
21 ∀ s : Finset I, s.Nonempty → ∃ j, ∀ i ∈ s, i ≤ j := by
22 classical
23 intro s
24 refine Finset.induction_on s ?_ ?_
25 · intro hs
26 rcases hs with ⟨i, hi⟩
27 simp only [Finset.notMem_empty] at hi
28 · intro a s ha ih hs
29 by_cases hs' : s.Nonempty
30 · rcases ih hs' with ⟨j, hj⟩
31 rcases hdir a j with ⟨k, hak, hjk⟩
32 refine ⟨k, ?_⟩
33 intro i hi
34 rw [Finset.mem_insert] at hi
35 rcases hi with rfl | hi
36 · exact hak
37 · exact (hj i hi).trans hjk
38 · have hs'' : s = ∅ := Finset.not_nonempty_iff_eq_empty.mp hs'
39 subst hs''
40 refine ⟨a, ?_⟩
41 intro i hi
42 simp only [insert_empty_eq, Finset.mem_singleton] at hi
43 simp only [hi, le_refl]
45end
47end ProCGroups.InverseSystems