dens_map_le — Mathlib

English

For an injective map f, the density of the image is bounded by the density of the domain.

Русский

При инъекции f плотность образа не превосходит плотности исходного множества.

LaTeX

$$$\\forall f:\\alpha \\hookrightarrow \\beta\\, (\\text{injective}),\\ \\mathrm{dens}(\\mathrm{map}\\, f\\, s) \\le \\mathrm{dens}(s)$$$

Lean4

theorem dens_map_le [Fintype β] (f : α ↪ β) : dens (s.map f) ≤ dens s :=
  by
  cases isEmpty_or_nonempty α
  · simp [Subsingleton.elim s ∅]
  simp_rw [dens, card_map]
  gcongr
  · exact mod_cast Fintype.card_pos
  · exact Fintype.card_le_of_injective _ f.2

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