submodulesBasisIsBasis — Mathlib

English

Given a RingFilterBasis BR and a BR.SubmodulesBasis B, one gets a SubmodulesBasis for BR.

Русский

Для BR и BR.SubmodulesBasis B получается SubmodulesBasis для BR.

LaTeX

$$BR.SubmodulesBasis B → SubmodulesBasis B$$

Lean4

theorem submodulesBasisIsBasis (BR : RingFilterBasis R) {B : ι → Submodule R M} (hB : BR.SubmodulesBasis B) :
    @_root_.SubmodulesBasis ι R _ M _ _ BR.topology B :=
  let _ := BR.topology
  { inter := hB.inter
    smul := by
      letI := BR.topology
      intro m i
      rcases hB.smul m i with ⟨V, V_in, hV⟩
      exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV }

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