coe_sInf — Mathlib

English

The underlying set of the infimum of a family of submonoids equals the intersection of the underlying sets of those submonoids.

Русский

Множество, лежащее в основе инфимума семейства подп monoid, равно пересечению их множеств.

LaTeX

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

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_sInf (S : Set (Submonoid M)) : ((sInf S : Submonoid M) : Set M) = ⋂ s ∈ S, ↑s :=
  rfl

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