ext

Mathlib.Topology.Sets.Closeds

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

English

The coercion applied to the constructor mk recovers the underlying set: (mk s h h') = s.

Русский

Преобразование через коэфункцию к конструктору mk восстанавливает основанное множество: (mk s h h') = s.

LaTeX

$$$(mk\ s\ h\ h' : \mathrm{Set}(\alpha)) = s$$$

Lean4

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

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

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

Разделы

Аффилиация

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