subset_union — Mathlib

English

A set-theoretic translation of subset containment for ideals: if the underlying set of I is contained in J ∪ K, then I ≤ J or I ≤ K.

Русский

Перевод на множества: если множество I содержится в J ∪ K, то I ≤ J или I ≤ K.

LaTeX

$$$ (I :\, \text{Set} R) \subseteq J \cup K \iff I \le J \lor I \le K $$$

Lean4

theorem subset_union {R : Type u} [Ring R] {I J K : Ideal R} : (I : Set R) ⊆ J ∪ K ↔ I ≤ J ∨ I ≤ K :=
  AddSubgroupClass.subset_union

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