finiteHeight_of_le — Mathlib

English

If J has finite height and I is contained in J (I ≤ J) with J not top, then I has finite height as well.

Русский

Если у идеала J конечная высота и I ⊆ J, причём J ≠ ⊤, то и I имеет конечную высоту.

LaTeX

$$$(I \le J) \land J \neq \top \land \operatorname{FiniteHeight}(J) \Rightarrow \operatorname{FiniteHeight}(I).$$$

Lean4

/-- If J has finite height and I ≤ J, then I has finite height -/
theorem finiteHeight_of_le {I J : Ideal R} (e : I ≤ J) (hJ : J ≠ ⊤) [FiniteHeight J] : FiniteHeight I where
  eq_top_or_height_ne_top :=
    Or.inr <| by
      rw [← lt_top_iff_ne_top]
      exact (height_mono e).trans_lt (height_lt_top hJ)

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