instInfSet

Mathlib.RingTheory.DividedPowers.SubDPIdeal

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

Lean4

instance : InfSet (SubDPIdeal hI) :=
  ⟨fun S ↦
    { carrier := ⨅ s ∈ Insert.insert ⊤ S, (s : hI.SubDPIdeal).carrier
      isSubideal := fun x hx ↦ by
        simp only [mem_iInf] at hx
        exact hx ⊤ (Set.mem_insert ⊤ S)
      dpow_mem := fun _ hn x hx ↦ by
        simp only [mem_iInf] at hx ⊢
        exact fun s hs ↦ s.dpow_mem _ hn x (hx s hs) }⟩

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

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

Разделы

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

Аффилиация

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