coe_sInf

Mathlib.Algebra.Module.Submodule.Lattice

URI: https://scilib.ai/kg/mathlib#Submodule.coe_sInf

English

The underlying set of sInf P equals the intersection of the underlying sets of all p ∈ P.

Русский

Множество-основа sInf P равно пересечению множеств p для всех p ∈ P.

LaTeX

$$$\uparrow(\mathrm{sInf}(P)) = \bigcap_{p \in P} \uparrow p$$$

Lean4

@[simp]
theorem coe_sInf (P : Set (Submodule R M)) : (↑(sInf P) : Set M) = ⋂ p ∈ P, ↑p :=
  rfl

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

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

Разделы

Аффилиация

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