mem_iInf

Mathlib.Algebra.Module.Submodule.Lattice

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

← MathLib Explorer

English

x ∈ iInf p iff ∀ i, x ∈ p(i).

Русский

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

LaTeX

$$$(x \in \mathrm{iInf}\, p) \iff \forall i, x \in p(i)$$$

Lean4

@[simp]
theorem mem_iInf {ι} (p : ι → Submodule R M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i := by
  rw [← SetLike.mem_coe, coe_iInf, Set.mem_iInter]; rfl

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

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

Разделы

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

Аффилиация

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