pimage_some

Mathlib.Data.Finset.PImage

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

← MathLib Explorer

English

For Finset s and function f, pimage of Part.some (f x) over s equals image f s.

Русский

Для Finset s и функции f, pimage Part.some(f x) над s равен image f s.

LaTeX

$$$(s.pimage (\lambda x. \text{Part.some}(f x))) = s.image f$.$$

Lean4

@[simp]
theorem pimage_some (s : Finset α) (f : α → β) [∀ x, Decidable (Part.some <| f x).Dom] :
    (s.pimage fun x => Part.some (f x)) = s.image f := by
  ext
  simp [eq_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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