English
Infimum of a family of LieSubmodules corresponds to the intersection of their underlying Submodules, with the Lie membership defined componentwise.
Русский
Наименьшая верхняя граница семейства Lie-подмодулей соответствует пересечению их подмножеств внутри M, причем условие замыкания держится по элементам.
LaTeX
$$$\text{InfSet}$-infimum of S corresponds to the intersection: \Big(\inf S\Big)^{toSubmodule} = \bigcap_{N\in S} N^{toSubmodule}$$$
Lean4
instance : InfSet (LieSubmodule R L M) :=
⟨fun S ↦
{ toSubmodule := sInf ({(s : Submodule R M) | s ∈ S})
lie_mem := fun {x m} h ↦
by
simp only [Submodule.mem_carrier, mem_iInter, Submodule.coe_sInf, mem_setOf_eq, forall_apply_eq_imp_iff₂,
forall_exists_index, and_imp] at h ⊢
intro N hN; apply N.lie_mem (h N hN) }⟩
