fiber_card_ne_zero_iff_mem_image — Mathlib

English

For S finite and f: A → B, for any y in B, the fiber {x ∈ S | f(x) = y} is nonempty if and only if y lies in the image of S under f.

Русский

Для конечного S и функции f: A → B,f(y) образует непустый волокно над y, если и только если y принадлежит образу S под f.

LaTeX

$$$\\#\\{x \\in S \\mid f(x) = y\\} \\neq 0 \\iff y \\in S image f$$$

Lean4

theorem fiber_card_ne_zero_iff_mem_image (s : Finset α) (f : α → β) [DecidableEq β] (y : β) :
    #(s.filter fun x ↦ f x = y) ≠ 0 ↔ y ∈ s.image f := by
  rw [← Nat.pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]

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