dens_image — Mathlib

English

Density is invariant under image of a bijection between finite types.

Русский

Плотность инвариантна по образу биекции между конечными типами.

LaTeX

$$$\\forall f:\\alpha \\to \\beta\\, (\\text{Bijective})\\; s:\\ Finset\\ \\alpha,\\ (s.image f).dens = s.dens$$$

Lean4

theorem dens_image [Fintype β] [DecidableEq β] {f : α → β} (hf : Bijective f) (s : Finset α) :
    (s.image f).dens = s.dens := by simpa [map_eq_image, -dens_map_equiv] using dens_map_equiv (.ofBijective f hf)

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