mem_iInf

Mathlib.Algebra.Ring.Subring.Basic

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

English

For any index set ι, x ∈ ⨅ i, S_i iff ∀ i, x ∈ S_i.

Русский

Для индекса ι верно: x ∈ ⨅ i, S_i тогда и только тогда, когда ∀ i, x ∈ S_i.

LaTeX

$$$x \\in \\bigcap_i S_i \\iff \\forall i, x \\in S_i$$$

Lean4

theorem mem_iInf {ι : Sort*} {S : ι → Subring R} {x : R} : (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i := by
  simp only [iInf, mem_sInf, Set.forall_mem_range]

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

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

Разделы

Аффилиация

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