extensionOfMax_to_submodule_eq_top

English

The domain of the maximal extension equals the whole ambient space; equivalently, the extension covers all of M (or the relevant ambient module) in the Baer setting.

Русский

Область определения максимального расширения равна всей окружающей подпростковой структуре; другими словами, расширение охватывает всё пространство в рамках условия Баера.

LaTeX

$$$ (\\mathrm{extensionOfMax}\\ i\\ f).\\mathrm{domain} = \\top $$$

Lean4

theorem extensionOfMax_to_submodule_eq_top (h : Module.Baer R Q) : (extensionOfMax i f).domain = ⊤ :=
  by
  refine Submodule.eq_top_iff'.mpr fun y => ?_
  dsimp
  rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin, Submodule.mem_sup]
  exact ⟨0, Submodule.zero_mem _, y, Submodule.mem_span_singleton_self _, zero_add _⟩

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