closure_le — Mathlib

English

For any s and t (t a nonunital subsemiring), closure(s) ≤ t iff s ⊆ t.

Русский

Для любых s и t (t — неединичный подсемиринг), closure(s) ≤ t тогда и только тогда, когда s ⊆ t.

LaTeX

$$$\mathrm{closure}(s) \le t \iff s \subseteq t$$$

Lean4

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

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