mem_insert_coe

Mathlib.Data.Finset.Insert

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

English

The membership in insert y s corresponds to membership in the Set insertion when s is viewed as a Set.

Русский

Членство в вставке соответствует членству в соответствующем множестве.

LaTeX

$$$ x \in insert y s \iff x \in insert y (s : Set\ α)$$$

Lean4

theorem mem_insert_coe {s : Finset α} {x y : α} : x ∈ insert y s ↔ x ∈ insert y (s : Set α) := by simp

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

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

Разделы

Аффилиация

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