isSubDPIdeal_iSup — Mathlib

English

If every J i is a sub-dp-ideal, then the supremum over i of J i (iSup J) is a sub-dp-ideal.

Русский

Если каждый J_i является под dp-идеалом, то их суммарная верхняя граница по индексу i (iSup J) также является под dp-идеалом.

LaTeX

$$IsSubDPIdeal hI (iSup J)$$

Lean4

theorem isSubDPIdeal_iSup {ι : Type*} {J : ι → Ideal A} (hJ : ∀ i, IsSubDPIdeal hI (J i)) : IsSubDPIdeal hI (iSup J) :=
  by
  rw [iSup_eq_span, span_isSubDPIdeal_iff (Set.iUnion_subset_iff.mpr <| fun i ↦ (hJ i).1)]
  simp_rw [Set.mem_iUnion]
  rintro n hn a ⟨i, ha⟩
  exact span_mono (Set.subset_iUnion _ i) (subset_span ((hJ i).2 n hn ha))

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