English
Every chain can be extended to a maximal chain; i.e., if c is a chain, there exists M which is maximal and contains c.
Русский
Любая цепь может быть расширена до максимальной цепи; то есть существует M, максимально в виде цепи, такая что c ⊆ M.
LaTeX
$$$$\forall {\alpha} {r} {c}, IsChain r c \to \exists M, \ IsMaxChain r M \land c \subseteq M.$$$$
Lean4
/-- Every chain is contained in a maximal chain. This generalizes Hausdorff's maximality principle.
-/
theorem exists_maxChain (hc : IsChain r c) : ∃ M, @IsMaxChain _ r M ∧ c ⊆ M :=
by
have H := zorn_subset_nonempty {s | c ⊆ s ∧ IsChain r s} ?_ c ⟨Subset.rfl, hc⟩
· obtain ⟨M, hcM, hM⟩ := H
exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩
rintro cs hcs₀ hcs₁ ⟨s, hs⟩
refine ⟨⋃₀ cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ => Set.subset_sUnion_of_mem⟩
rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz
obtain rfl | hsseq := eq_or_ne sy sz
· exact (hcs₀ hsy).right hysy hzsz hyz
rcases hcs₁ hsy hsz hsseq with h | h
· exact (hcs₀ hsz).right (h hysy) hzsz hyz
· exact (hcs₀ hsy).right hysy (h hzsz) hyz
