Module

Utilities.lean

Nyll.ProCGroups.InverseSystems.Utilities

1 declaration indexed from sourceView source ↗

Module documentation

Order-theoretic utilities for inverse systems

The finite-upper-bound lemma in this module turns directedness of a preorder into a single stage dominating any nonempty finite set of indices. It is the common combinatorial step in compactness, cofinality, and finite-coordinate arguments for inverse limits.

Imports1

Mathlib.Topology.Homeomorph.Lemmas

Imported by3

theorem

exists_upperBound_finset

L26 ↗

ProCGroups.InverseSystems.exists_upperBound_finset

Documentation

A finite subset of a directed preorder admits an upper bound.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.InverseSystems
universe u
section
variable {I : Type u} [Preorder I]

Lean source · statement

theorem exists_upperBound_finset (hdir : Directed (· ≤ ·) (id : I → I)) :
    ∀ s : Finset I, s.Nonempty → ∃ j, ∀ i ∈ s, i ≤ j

Module documentation

Order-theoretic utilities for inverse systems

Declarations

exists_upperBound_finset