sInf_toAddSubgroup — Mathlib

English

The Infimum of a family of nonunital subrings, as an AddSubgroup, is the infimum of their corresponding AddSubgroups.

Русский

Infimum семейства подподкольц без единицы в виде AddSubgroup равен инфимуму по AddSubgroups.

LaTeX

$$$$ (sInf\, s).toAddSubgroup = \\big(\\bigwedge t \\in s, Subgroup t\\big). $$$$

Lean4

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

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