coe_mem

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.coe_mem

English

If x ∈ s.toSet.Elem, then x.val ∈ s.

Русский

Если x принадлежит элементу x ∈ s.toSet.Elem, то x.val принадлежит s.

LaTeX

$$$ \uparrow x \in s $$$

Lean4

@[simp]
theorem coe_mem {s : Finset α} (x : (s : Set α)) : ↑x ∈ s :=
  x.2

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

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

Разделы

Аффилиация

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