ext

Mathlib.Order.CompleteLattice.SetLike

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

English

In a CompleteSublattice, extensionality holds: two subobjects are equal if they have the same elements.

Русский

В CompleteSublattice экстенсиональность: две подструктуры равны, если они содержат одни и те же элементы.

LaTeX

$$$\\text{ext} :\\; (\\forall x, x \\in S \\iff x \\in T) \\Rightarrow S = T$$$

Lean4

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

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

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

Разделы

Аффилиация

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