mem_carrier — Mathlib

English

For a SubMulAction p, membership of x in the carrier equals membership in the underlying set of p.

Русский

Для SubMulAction p принадлежность x ко внутрику носителя эквивалентна принадлежности x к базовому множеству p.

LaTeX

$$$x \\in p.carrier \\iff x \\in (p : Set M)$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_carrier {p : SubMulAction R M} {x : M} : x ∈ p.carrier ↔ x ∈ (p : Set M) :=
  Iff.rfl

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