mathlib documentation

order.compactly_generated

Compactness properties for complete lattices #

For complete lattices, there are numerous equivalent ways to express the fact that the relation > is well-founded. In this file we define three especially-useful characterisations and provide proofs that they are indeed equivalent to well-foundedness.

Main definitions #

Main results #

The main result is that the following four conditions are equivalent for a complete lattice:

This is demonstrated by means of the following four lemmas:

We also show well-founded lattices are compactly generated (complete_lattice.compactly_generated_of_well_founded).

References #

Tags #

complete lattice, well-founded, compact

def complete_lattice.is_sup_closed_compact (α : Type u_1) [complete_lattice α] :
Prop

A compactness property for a complete lattice is that any sup-closed non-empty subset contains its Sup.

Equations
def complete_lattice.is_Sup_finite_compact (α : Type u_1) [complete_lattice α] :
Prop

A compactness property for a complete lattice is that any subset has a finite subset with the same Sup.

Equations
def complete_lattice.is_compact_element {α : Type u_1} [complete_lattice α] (k : α) :
Prop

An element k of a complete lattice is said to be compact if any set with Sup above k has a finite subset with Sup above k. Such an element is also called "finite" or "S-compact".

Equations
theorem complete_lattice.is_compact_element_iff_le_of_directed_Sup_le (α : Type u_1) [complete_lattice α] (k : α) :
complete_lattice.is_compact_element k ∀ (s : set α), s.nonemptydirected_on has_le.le sk Sup s(∃ (x : α), x s k x)

An element k is compact if and only if any directed set with Sup above k already got above k at some point in the set.

theorem complete_lattice.is_compact_element.directed_Sup_lt_of_lt {α : Type u_1} [complete_lattice α] {k : α} (hk : complete_lattice.is_compact_element k) {s : set α} (hemp : s.nonempty) (hdir : directed_on has_le.le s) (hbelow : ∀ (x : α), x sx < k) :
Sup s < k

A compact element k has the property that any directed set lying strictly below k has its Sup strictly below k.

theorem complete_lattice.finset_sup_compact_of_compact {α : Type u_1} {β : Type u_2} [complete_lattice α] {f : β → α} (s : finset β) (h : ∀ (x : β), x scomplete_lattice.is_compact_element (f x)) :

Alias of well_founded_iff_is_Sup_finite_compact.

Alias of is_Sup_finite_compact_iff_is_sup_closed_compact.

Alias of is_sup_closed_compact_iff_well_founded.

@[class]
structure is_compactly_generated (α : Type u_2) [complete_lattice α] :
Prop

A complete lattice is said to be compactly generated if any element is the Sup of compact elements.

Instances
@[simp]
theorem Sup_compact_le_eq {α : Type u_1} [complete_lattice α] [is_compactly_generated α] (b : α) :
theorem le_iff_compact_le_imp {α : Type u_1} [complete_lattice α] [is_compactly_generated α] {a b : α} :
a b ∀ (c : α), complete_lattice.is_compact_element cc ac b
theorem inf_Sup_eq_of_directed_on {α : Type u_1} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} (h : directed_on has_le.le s) :
a Sup s = ⨆ (b : α) (H : b s), a b

This property is sometimes referred to as α being upper continuous.

theorem inf_Sup_eq_supr_inf_sup_finset {α : Type u_1} [complete_lattice α] [is_compactly_generated α] {a : α} {s : set α} :
a Sup s = ⨆ (t : finset α) (H : t s), a t.sup id

This property is equivalent to α being upper continuous.

theorem complete_lattice.set_independent_Union_of_directed {α : Type u_1} [complete_lattice α] [is_compactly_generated α] {η : Type u_2} {s : η → set α} (hs : directed has_subset.subset s) (h : ∀ (i : η), complete_lattice.set_independent (s i)) :

A compact element k has the property that any b <k lies below a "maximal element below k", which is to say [⊥, k] is coatomic.

@[protected, instance]
@[protected, instance]

See Lemma 5.1, Călugăreanu

See Theorem 6.6, Călugăreanu

See Theorem 6.6, Călugăreanu