ext

Mathlib.Order.Sublocale

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

English

If two Sublocales have exactly the same membership for every element x, then they are equal.

Русский

Если для всех элементов x выполняется x ∈ S ↔ x ∈ T, то S = T.

LaTeX

$$$( \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