mem_carrier — Mathlib

English

For a StarSubsemiring S, membership to its carrier equals membership to S itself: x ∈ S.carrier iff x ∈ S.

Русский

Для StarSubsemiring S принадлежность элементу к носителю S эквивалентна принадлежности самому S: x ∈ S.carrier ↔ x ∈ S.

LaTeX

$$$ x \in S.\text{carrier} \;\Leftrightarrow\; x \in S $$$

Lean4

theorem mem_carrier {s : StarSubsemiring R} {x : R} : x ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl

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