fiber_nonempty_iff_mem_image

Mathlib.Data.Finset.Image

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

English

For any y in β, the fiber {a ∈ s | f a = y} is nonempty iff y ∈ s.image f.

Русский

Для любого y в β множество элементов a ∈ s с f(a) = y не пусто тогда и только тогда, когда y ∈ image f s.

LaTeX

$$$(s \cap \{a : f(a) = y\}).Nonempty \iff y \in s.image f$$$

Lean4

theorem fiber_nonempty_iff_mem_image {y : β} : (s.filter (f · = y)).Nonempty ↔ y ∈ s.image f := by
  simp [Finset.Nonempty]

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

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

Разделы

Аффилиация

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