English
Every nonempty family of finite character has a maximal element: given F with IsOfFiniteCharacter and x ∈ F, there exists m with x ⊆ m and m is maximal in F.
Русский
У каждой непустой семьи с конечным характером есть максимальный элемент: если F имеет IsOfFiniteCharacter и x ∈ F, то существует m с x ⊆ m и m максимален в F.
LaTeX
$$$\\forall F:\\\\ Set(Set α),\\\\ IsOfFiniteCharacter F \\rightarrow \\\\forall x:\\\\ Set α, x\\in F \\rightarrow \\\\exists m:\\\\ Set α, x \\subseteq m \\land m\\in F \\land \\forall n:\\\\ Set α, n\\in F \\land x\\subseteq n \\rightarrow n = m$$$
Lean4
/-- **Teichmuller-Tukey lemma**. Every nonempty family of finite character has a maximal element. -/
theorem exists_maximal {F} (hF : IsOfFiniteCharacter F) {x : Set α} (xF : x ∈ F) : ∃ m, x ⊆ m ∧ Maximal (· ∈ F) m := by
/- Apply Zorn's lemma. Take the union of the elements of a chain as its upper bound. -/
refine zorn_subset_nonempty F (fun c cF cch cne ↦ ⟨sUnion c, ?_, fun s sc ↦ subset_sUnion_of_mem sc⟩) x xF
refine
(hF (sUnion c)).mpr fun s sc sfin ↦
?_
/- Use the finite character property and the fact that any finite subset of the union is also a
subset of some element of the chain. -/
obtain ⟨t, tc, st⟩ := cch.directedOn.exists_mem_subset_of_finite_of_subset_sUnion cne sfin sc
exact (hF t).mp (cF tc) s st sfin
