closure_le — Mathlib

English

Underlying set of the Infimum of a family of submonoids equals the intersection of their underlying sets (alternate form).

Русский

Основа множества инфимума семейства подпмонов равна пересечению их оснований.

LaTeX

$$((sInf S : Submonoid M) : Set M) = ⋂ s ∈ S, ↑s$$

Lean4

/-- A submonoid `S` includes `closure s` if and only if it includes `s`. -/
@[to_additive (attr := simp) /-- An additive submonoid `S` includes `closure s` if and only if it includes `s`. -/
    ]
theorem closure_le : closure s ≤ S ↔ s ⊆ S :=
  ⟨Subset.trans subset_closure, fun h => sInf_le h⟩

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