mk_le_mk_mul_of_mk_preimage_le — Mathlib

English

If for every b, the size of the preimage f^{-1}({b}) is ≤ c, then #α ≤ #β · c.

Русский

Если для каждого b множества f^{-1}({b}) имеет размер ≤ c, то #α ≤ #β · c.

LaTeX

$$$\\forall b, \\lvert f^{-1} \\{b\\} \\rvert \\le c \\;\Rightarrow\\; \\lvert \\alpha \\rvert \\le \\lvert \\beta \\rvert \\cdot c$$$

Lean4

theorem mk_le_mk_mul_of_mk_preimage_le {c : Cardinal} (f : α → β) (hf : ∀ b : β, #(f ⁻¹' { b }) ≤ c) : #α ≤ #β * c := by
  simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using sum_le_sum _ _ hf

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