isSubDPIdeal_iInf — Mathlib

English

If every J i is a sub-dp-ideal, then I ∧ iInf J i (iInf of J i) is a sub-dp-ideal.

Русский

Если каждый J_i является под dp-идеалом, то огибающая I ∧ (пересечение J_i) является под dp-идеалом.

LaTeX

$$IsSubDPIdeal hI (I ⊓ iInf (fun i ↦ J i))$$

Lean4

theorem isSubDPIdeal_iInf {ι : Type*} {J : ι → Ideal A} (hJ : ∀ i, IsSubDPIdeal hI (J i)) :
    IsSubDPIdeal hI (I ⊓ iInf (fun i ↦ J i)) := by
  cases isEmpty_or_nonempty ι with
  | inr _ =>
    refine ⟨fun _ hx ↦ hx.1, ?_⟩
    intro n hn x hx
    simp only [Ideal.mem_inf, mem_iInf] at hx ⊢
    exact ⟨hI.dpow_mem hn hx.1, fun i ↦ IsSubDPIdeal.dpow_mem (hJ i) n hn (hx.2 i)⟩
  | inl _ =>
    simp only [iInf_of_empty, le_top, inf_of_le_left]
    exact IsSubDPIdeal.self hI

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