sInf_carrier_def

Mathlib.RingTheory.DividedPowers.SubDPIdeal

URI: https://scilib.ai/kg/mathlib#DividedPowers.SubDPIdeal.sInf_carrier_def

English

The carrier of the infimum J ⊓ J' is the intersection of their carriers.

Русский

Носитель (carrier) наименьшего элемента (infimum) J ⊓ J' равен пересечению носителей J и J'.

LaTeX

$$$(J \sqcap J').carrier = J.carrier \cap J'.carrier$$

Lean4

theorem sInf_carrier_def (S : Set (SubDPIdeal hI)) :
    (sInf S).carrier = ⨅ s ∈ Insert.insert ⊤ S, (s : hI.SubDPIdeal).carrier :=
  rfl

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

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

Разделы

Аффилиация

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