closure_eq_of_isClosed — Mathlib

English

If the underlying set of an ideal I is closed in R, then its closure as an ideal equals I itself.

Русский

Если множество, лежащее в I, замкнуто в R, то замыкание I как идеала равно самому I.

LaTeX

$$I.closure = I$$

Lean4

/-- This is not `@[simp]` since otherwise it causes timeouts downstream as `simp` tries and fails to
generate an `IsClosed` instance.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234852.20heartbeats.20of.20the.20linter
-/
theorem closure_eq_of_isClosed (I : Ideal R) (hI : IsClosed (I : Set R)) : I.closure = I :=
  SetLike.ext' hI.closure_eq

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