isSubDPIdeal_sup — Mathlib

English

If J and K are sub-dp-ideals, then their supremum J ⊔ K is also a sub-dp-ideal.

Русский

Если J и K — под dp-идеалы, то их суммарное объединение J ⊔ K также является под dp-идеалом.

LaTeX

$$IsSubDPIdeal hI (J ⊔ K)$$

Lean4

theorem isSubDPIdeal_sup {J K : Ideal A} (hJ : IsSubDPIdeal hI J) (hK : IsSubDPIdeal hI K) : IsSubDPIdeal hI (J ⊔ K) :=
  by
  rw [← J.span_eq, ← K.span_eq, ← span_union, span_isSubDPIdeal_iff (Set.union_subset_iff.mpr ⟨hJ.1, hK.1⟩)]
  intro n hn a ha
  rcases ha with ha | ha
  · exact span_mono Set.subset_union_left (subset_span (hJ.2 n hn ha))
  · exact span_mono Set.subset_union_right (subset_span (hK.2 n hn ha))

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