mem_carrier

Mathlib.Order.Sublocale

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

English

An element a belongs to the carrier of a Sublocale X iff a belongs to X.

Русский

Элемент a принадлежит носителю подокруга Sublocale X тогда и только тогда, когда a принадлежит самому X.

LaTeX

$$$a \in X. carrier \Leftrightarrow a \in X$$$

Lean4

@[simp]
theorem mem_carrier : a ∈ S.carrier ↔ a ∈ S :=
  .rfl

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

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

Разделы

Аффилиация

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