ext

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.PositiveCompacts.ext

English

Two PositiveCompacts with the same underlying set are equal.

Русский

Два PositiveCompacts с одинаковым носителем равны.

LaTeX

$$$ \text{ext}\;{s,t}: (s : \mathrm{Set}\alpha) = (t : \mathrm{Set}\alpha) \Rightarrow s = t$$$

Lean4

@[ext]
protected theorem ext {s t : PositiveCompacts α} (h : (s : Set α) = t) : s = t :=
  SetLike.ext' h

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

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

Разделы

Аффилиация

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