Teichmuller-Tukey

This file defines the notion of being of finite character for a family of sets and proves the Teichmuller-Tukey lemma.

Main definitions

• IsOfFiniteCharacter : A family of sets $F$ is of finite character iff for every set $X$, $X ∈ F$ iff every finite subset of $X$ is in $F$.

Main results

• IsOfFiniteCharacter.exists_maximal : Teichmuller-Tukey lemma, saying that every nonempty family of finite character has a maximal element.

References

• https://en.wikipedia.org/wiki/Teichm%C3%BCller%E2%80%93Tukey_lemma

def Order.IsOfFiniteCharacter {α : Type u_1} (F : Set (Set α)) : Prop

A family of sets $F$ is of finite character iff for every set $X$, $X ∈ F$ iff every finite subset of $X$ is in $F$

Equations

• Order.IsOfFiniteCharacter F = ∀ (x : Set α), x ∈ F ↔ ∀ y ⊆ x, y.Finite → y ∈ F

theorem Order.IsOfFiniteCharacter.exists_maximal {α : Type u_1} {F : Set (Set α)} (hF : IsOfFiniteCharacter F) {x : Set α} (xF : x ∈ F) : ∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) => x ∈ F) m

Teichmuller-Tukey lemma. Every nonempty family of finite character has a maximal element.