mem_finsetInf

Mathlib.Algebra.Module.Submodule.Lattice

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

← MathLib Explorer

English

x ∈ s.inf p iff ∀ i ∈ s, x ∈ p(i).

Русский

x принадлежит s.inf p тогда и только тогда, когда для каждого i в s x ∈ p(i).

LaTeX

$$$x \in s.\inf p \iff \forall i \in s, x \in p(i)$$$

Lean4

@[simp]
theorem mem_finsetInf {ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} : x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i := by
  simp only [← SetLike.mem_coe, coe_finsetInf, Set.mem_iInter]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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