mem_toFinset

Mathlib.Data.Finset.PImage

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

English

For any Part o of α, and any x ∈ α, x belongs to o.toFinset if and only if x ∈ o.

Русский

Пусть o — часть α. Тогда x принадлежит o.toFinset тогда и только тогда, когда x принадлежит o.

LaTeX

$$$x \in o.toFinset \iff x \in o$.$$

Lean4

@[simp]
theorem mem_toFinset {o : Part α} [Decidable o.Dom] {x : α} : x ∈ o.toFinset ↔ x ∈ o := by simp [toFinset]

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

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

Разделы

Аффилиация

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