extensionOfMax_is_max — Mathlib

English

The maximal extension is indeed maximal: if an extension a satisfies extensionOfMax ≤ a, then a = extensionOfMax.

Русский

Максимальное расширение действительно максимальное: если a удовлетворяет extensionOfMax ≤ a, то a = extensionOfMax.

LaTeX

$$$ \forall a: \mathrm{ExtensionOf}(i,f),\ a \ge \mathrm{extensionOfMax}(i,f) \Rightarrow a = \mathrm{extensionOfMax}(i,f)$$$

Lean4

theorem extensionOfMax_is_max : ∀ (a : ExtensionOf i f), extensionOfMax i f ≤ a → a = extensionOfMax i f := fun _ ↦
  (@zorn_le_nonempty (ExtensionOf i f) _ ⟨Inhabited.default⟩ fun _ hchain hnonempty =>
      ⟨ExtensionOf.max hchain hnonempty, ExtensionOf.le_max hchain hnonempty⟩).choose_spec.eq_of_ge

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