extensionOfMax — Mathlib

English

For a chain c of Baer extensions, the max extension is an upper bound for all elements of the chain.

Русский

Для цепи расширений Баера верхняя граница максимумом является над всеми элементами цепи.

LaTeX

$$$ \forall a \in c: a \le \mathrm{ExtensionOf.max}(hchain,hnonempty)$$$

Lean4

/-- Since every nonempty chain has a maximal element, by Zorn's lemma, there is a maximal
`extension_of i f`. -/
def extensionOfMax : ExtensionOf i f :=
  (@zorn_le_nonempty (ExtensionOf i f) _ ⟨Inhabited.default⟩ fun _ hchain hnonempty =>
      ⟨ExtensionOf.max hchain hnonempty, ExtensionOf.le_max hchain hnonempty⟩).choose

Похожие утверждения