sInf_toAddSubgroup — Mathlib

English

The infimum of a set of subrings, when viewed as additive subgroups, equals the infimum taken over AddSubgroup components.

Русский

Наименьшее подкольцо в виде аддитивных подгрупп совпадает с инфимумом по компонентам AddSubgroup.

LaTeX

$$$\\big( sInf\\; S \\right).toAddSubgroup = \\inf_{t∈S} t.toAddSubgroup$$$

Lean4

@[simp]
theorem sInf_toAddSubgroup (s : Set (Subring R)) : (sInf s).toAddSubgroup = ⨅ t ∈ s, Subring.toAddSubgroup t :=
  mk'_toAddSubgroup _ _

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