English
For submodule N and sets s, t ⊆ S, (s ⊔ t) • N = s • N ⊔ t • N, i.e., the action distributes over the lattice join.
Русский
Для подмодуля N и множеств s, t ⊆ S верно (s ⊔ t) • N = s • N ⊔ t • N, т.е. действие распределяется по объединению верхних граней.
LaTeX
$$$ (s \lor t) \cdot N = s \cdot N \lor t \cdot N $$$
Lean4
/-- In a ring, sets acts on submodules. -/
protected noncomputable def pointwiseSetDistribMulAction [SMulCommClass R R M] :
DistribMulAction (Set R) (Submodule R M)
where
smul_zero s := set_smul_bot s
smul_add s x
y :=
le_antisymm
(set_smul_le _ _ _ <| by
rintro r m hr hm
rw [add_eq_sup, Submodule.mem_sup] at hm
obtain ⟨a, ha, b, hb, rfl⟩ := hm
rw [smul_add, add_eq_sup, Submodule.mem_sup]
exact
⟨r • a, mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := ha), r • b,
mem_set_smul_of_mem_mem (mem1 := hr) (mem2 := hb), rfl⟩)
(sup_le_iff.mpr ⟨smul_mono_right _ le_sup_left, smul_mono_right _ le_sup_right⟩)
