closure_le — Mathlib

English

The closure operator is order-preserving in the second argument: closure(s) ≤ t iff s ⊆ t, for t a NonUnitalSubring.

Русский

Замыкание сохраняет порядок: closure(s) ≤ t тогда и только тогда, когда s ⊆ t, где t — подпольцо.

LaTeX

$$$closure(s) \\le t \\iff s \\subseteq t$$$

Lean4

/-- A `NonUnitalSubring` `t` includes `closure s` if and only if it includes `s`. -/
@[simp]
theorem closure_le {s : Set R} {t : NonUnitalSubring R} : closure s ≤ t ↔ s ⊆ t :=
  ⟨Set.Subset.trans subset_closure, fun h => sInf_le h⟩

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