sInf_toAddSubmonoid — Mathlib

English

Similarly to Submonoid, the infimum of a set of subsemirings, viewed as add-submonoids, equals the infimum of the corresponding add-submonoids.

Русский

Аналогично подмножеству Submonoid, наименьшее над множеством подsemiring, рассмотренное как AddSubmonoid, равно соответствующему Inf.

LaTeX

$$$ (sInf S).toAddSubmonoid = \iInf t \in S, Subsemiring.toAddSubmonoid t $$$

Lean4

@[simp]
theorem sInf_toAddSubmonoid (s : Set (Subsemiring R)) :
    (sInf s).toAddSubmonoid = ⨅ t ∈ s, Subsemiring.toAddSubmonoid t :=
  mk'_toAddSubmonoid _ _

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