inf_mem

Mathlib.Algebra.Module.Submodule.Invariant

URI: https://scilib.ai/kg/mathlib#Module.End.invtSubmodule.inf_mem

English

If p and q are f-invariant, then their intersection is f-invariant.

Русский

Если p и q инвариантны по f, то их пересечение тоже инвариантно по f.

LaTeX

$$inf_mem: p ∈ f.invtSubmodule ∧ q ∈ f.invtSubmodule → p ⊓ q ∈ f.invtSubmodule$$

Lean4

theorem inf_mem {p q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : p ⊓ q ∈ f.invtSubmodule :=
  Sublattice.inf_mem hp hq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru