closure_le — Mathlib

English

Closure is monotone with respect to inclusion: if s ⊆ t, then closure(s) ≤ closure(t).

Русский

Замыкание монотонно по включению: если s ⊆ t, то closure(s) ≤ closure(t).

LaTeX

$$$\\operatorname{closure}(s) \\leq \\operatorname{closure}(t) \\;\\text{whenever}\\; s \\subseteq t$$$

Lean4

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

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