mem_carrier — Mathlib

English

Let S be a Subsemigroup of M and x a member of M. Then x is in the carrier of S if and only if x is in S.

Русский

Пусть S — подполугруппа M. Тогда для любого x ∈ M выполняется: x ∈ носитель(S) тогда же, что и x ∈ S.

LaTeX

$$$ x \\in \\operatorname{carrier}(S) \\iff x \\in S $$$

Lean4

@[to_additive (attr := simp)]
theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

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