mem

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Subtype.mem

English

If p is an element of the subtype s, then the underlying α-value of p lies in s.

Русский

Если p — элемент подтипа s, то значение p в α принадлежит s.

LaTeX

$$$\forall (p : s), (p : \alpha) \in s$$$

Lean4

/-- See also `Subtype.prop` -/
theorem mem {α : Type*} {s : Set α} (p : s) : (p : α) ∈ s :=
  p.prop

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

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

Разделы

Аффилиация

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