symm_eq_toNucleus

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#nucleusIsoSublocale.symm_eq_toNucleus

English

The sublocale-to-nucleus map is the inverse of the nucleus-to-sublocale isomorphism.

Русский

Обратная карта сублокалы к нуклеусу является обратной к изоморфизму нуклеуса к сублокале.

LaTeX

$$$\mathrm{Sublocale.toNucleus} = (\mathrm{nucleusIsoSublocale})^{-1}$$$

Lean4

theorem symm_eq_toNucleus : Sublocale.toNucleus = (@nucleusIsoSublocale X _).symm :=
  rfl

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

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

Разделы

Аффилиация

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