English
Let R and A be commutative rings with an A-algebra structure, V an additive group with R- and A-module structures and an IsScalarTower R A V. If M and N are submodules of V that are lattices over A, then their supremum M ⊔ N is also a lattice over A.
Русский
Пусть R и A — коммутативные кольца с тензорной структурой над A, V — аддитивная группа с модульными структурами над R и над A и с тензорной связью IsScalarTower R A V. Если M и N — подпроствольники V, являющиеся решётками над A, то их супремум M ⊔ N также является решёткой над A.
LaTeX
$$$IsLattice_A(M \sqcup N)$$$
Lean4
/-- The supremum of two lattices is a lattice. -/
instance sup (M N : Submodule R V) [IsLattice A M] [IsLattice A N] : IsLattice A (M ⊔ N) :=
of_le_of_isLattice_of_fg A le_sup_left (Submodule.FG.sup IsLattice.fg IsLattice.fg)
