Lean4
/-- The image of a submodules basis is a module filter basis. -/
def toModuleFilterBasis : ModuleFilterBasis R M
where
sets := {U | ∃ i, U = B i}
nonempty := by
inhabit ι
exact ⟨B default, default, rfl⟩
inter_sets := by
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
obtain ⟨k, hk⟩ := hB.inter i j
use B k
constructor
· use k
· exact hk
zero' := by
rintro _ ⟨i, rfl⟩
exact (B i).zero_mem
add' := by
rintro _ ⟨i, rfl⟩
use B i
constructor
· use i
· rintro x ⟨y, y_in, z, z_in, rfl⟩
exact (B i).add_mem y_in z_in
neg' := by
rintro _ ⟨i, rfl⟩
use B i
constructor
· use i
· intro x x_in
exact (B i).neg_mem x_in
conj' := by
rintro x₀ _ ⟨i, rfl⟩
use B i
constructor
· use i
· simp
smul' := by
rintro _ ⟨i, rfl⟩
use univ
constructor
· exact univ_mem
· use B i
constructor
· use i
· rintro _ ⟨a, -, m, hm, rfl⟩
exact (B i).smul_mem _ hm
smul_left' := by
rintro x₀ _ ⟨i, rfl⟩
use B i
constructor
· use i
· intro m
exact (B i).smul_mem _
smul_right' := by
rintro m₀ _ ⟨i, rfl⟩
exact hB.smul m₀ i
