mem_toSublocale

Mathlib.Order.Sublocale

URI: https://scilib.ai/kg/mathlib#Nucleus.mem_toSublocale

English

An element x belongs to the sublocale associated to n exactly when there exists y with n(y) = x.

Русский

Элемент x принадлежит сублокале, ассоциированной с n, если существует y с n(y) = x.

LaTeX

$$$x \in n^{\mathrm{toSublocale}} \;\iff\; \exists y,\ n(y) = x$$$

Lean4

@[simp]
theorem mem_toSublocale {n : Nucleus X} {x : X} : x ∈ n.toSublocale ↔ ∃ y, n y = x :=
  .rfl

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

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

Разделы

Аффилиация

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