ext

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Substructure.ext

← MathLib Explorer

English

Two substructures are equal if and only if they have the same elements.

Русский

Две подструктуры равны тогда, когда у них совпадают элементы.

LaTeX

$$$$ (\forall x, x \in S \iff x \in T) \Rightarrow S = T $$$$

Lean4

/-- Two substructures are equal if they have the same elements. -/
@[ext]
theorem ext {S T : L.Substructure M} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :=
  SetLike.ext h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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