English
The Baer extension structure is an inductive family of partial linear maps extending i to f, with domain a submodule of N and a corresponding map to Q compatible with i and f.
Русский
Структура расширения Баера — это семейство частичных линейных отображений, расширяющее i до f, где область определённости подмодуль N и существует соответствующее отображение в Q совместимое с i и f.
LaTeX
$$$ \text{Module.Baer.ExtensionOf } i f$ is the type of triples $(\text{domain}, \text{toLinearPMap}, \text{le})$ with compatibility conditions.$$
Lean4
theorem le_max {c : Set (ExtensionOf i f)} (hchain : IsChain (· ≤ ·) c) (hnonempty : c.Nonempty) (a : ExtensionOf i f)
(ha : a ∈ c) : a ≤ ExtensionOf.max hchain hnonempty :=
LinearPMap.le_sSup (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain) <|
(Set.mem_image _ _ _).mpr ⟨a, ha, rfl⟩
