sInf_toSubmonoid — Mathlib

English

The infimum of a set of subsemirings, taken as a submonoid, equals the infimum of the submonoids obtained from each member of the set.

Русский

Наименьшее над множеством подsemiring, взятое как подмоном, равно наименьшему над подмоном, полученному из каждого элемента множества.

LaTeX

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

Lean4

@[simp]
theorem sInf_toSubmonoid (s : Set (Subsemiring R)) : (sInf s).toSubmonoid = ⨅ t ∈ s, Subsemiring.toSubmonoid t :=
  mk'_toSubmonoid _ _

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