toIdeal_sup — Mathlib

English

The toIdeal map preserves both sup and inf: (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal and (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal.

Русский

Отображение toIdeal сохраняет и верхний, и нижний предел: (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal и (I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal.

LaTeX

$$$(I \\sqcup J).toIdeal = I.toIdeal \\sqcup J.toIdeal$ and $(I \\cap J).toIdeal = I.toIdeal \\cap J.toIdeal$$$

Lean4

@[simp]
theorem toIdeal_sup (I J : HomogeneousIdeal 𝒜) : (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal :=
  rfl

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