coe_sInf — Mathlib

English

The set-theoretic image of the infimum (sInf) of a set of subsemigroups equals the intersection of their carriers.

Русский

Образ инфима (sInf) множества подполугрупп по множеству эквиваленций равен пересечению множеств носителей.

LaTeX

$$$((sInf S) : Subsemigroup M) : Set M = \\bigcap S \\in S, \\uparrow S$$$

Lean4

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

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