homogeneousHull_mono — Mathlib

English

The map I ↦ Ideal.homogeneousHull 𝒜 I is monotone with respect to inclusion.

Русский

Отображение I ↦ Ideal.homogeneousHull 𝒜 I монотонно по включению.

LaTeX

$$$ I \le J \Rightarrow Ideal.homogeneousHull 𝒜 I \le Ideal.homogeneousHull 𝒜 J $$$

Lean4

theorem homogeneousHull_mono : Monotone (Ideal.homogeneousHull 𝒜) := fun I J I_le_J =>
  by
  apply Ideal.span_mono
  rintro r ⟨hr1, ⟨x, hx⟩, rfl⟩
  exact ⟨hr1, ⟨⟨x, I_le_J hx⟩, rfl⟩⟩

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