ext

Mathlib.GroupTheory.GroupAction.SubMulAction

URI: https://scilib.ai/kg/mathlib#SubMulAction.ext

English

Two SubMulActions are equal if they have the same membership relation on all elements.

Русский

Два SubMulAction равны, если для каждого элемента верно равносоотношение принадлежности.

LaTeX

$$$\\forall x, x \\in p \\iff x \\in q \\;\\Rightarrow\\; p = q$$$

Lean4

@[to_additive (attr := ext)]
theorem ext {p q : SubMulAction R M} (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
  SetLike.ext h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru