mem_toFinset

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Set.mem_toFinset

English

An element belongs to the Finset enumeration of s iff it belongs to s.

Русский

Элемент принадлежит перечислению Finset множества s тогда и только тогда, когда он принадлежит самому s.

LaTeX

$$$\forall a,\ a \in s.toFinset \iff a \in s$$$

Lean4

@[simp]
theorem mem_toFinset {s : Set α} [Fintype s] {a : α} : a ∈ s.toFinset ↔ a ∈ s := by simp [toFinset]

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

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

Разделы

Аффилиация

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