mem_sInf

Mathlib.Algebra.Star.Subalgebra

URI: https://scilib.ai/kg/mathlib#StarSubalgebra.mem_sInf

← MathLib Explorer

English

An element x lies in sInf S iff x lies in every member p of S.

Русский

Элемент x принадлежит sInf S тогда и только тогда, когда x принадлежит каждому члену S.

LaTeX

$$$x\in sInf S \iff \forall p\in S, x\in p$$$

Lean4

theorem mem_sInf {S : Set (StarSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p := by
  simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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

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

Разделы

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

Аффилиация

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