ext

Mathlib.Algebra.Module.Submodule.Defs

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

English

Two submodules are equal if they have the same elements; extensionality principle.

Русский

Два подмодуля равны, если совпадает их множество элементов; принцип экстенсиональности.

LaTeX

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

Lean4

@[ext]
theorem ext (h : ∀ x, x ∈ p ↔ x ∈ q) : p = q :=
  SetLike.ext h

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

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

Разделы

Аффилиация

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