mem_iSup_of_mem

Mathlib.RingTheory.Ideal.Lattice

URI: https://scilib.ai/kg/mathlib#Ideal.mem_iSup_of_mem

English

If i is a member of index set and x ∈ S(i), then x ∈ iSup S.

Русский

Если i принадлежит индексу, и x ∈ S(i), то x ∈ iSup S.

LaTeX

$$$\\\\forall i, x \\\\in S(i) \\\\Rightarrow x \\\\in iSup S$$$

Lean4

theorem mem_iSup_of_mem {ι : Sort*} {S : ι → Ideal R} (i : ι) : ∀ {x : R}, x ∈ S i → x ∈ iSup S :=
  @le_iSup _ _ _ S _

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

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

Разделы

Аффилиация

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