dens_map_equiv

Mathlib.Data.Finset.Density

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

English

Density is preserved under a finite type equivalence.

Русский

Плотность сохраняется при эквивалентности конечного типа.

LaTeX

$$$\\forall e:\\alpha \\simeq \\beta,\\ (s.map e.toEmbedding).dens = s.dens$$$

Lean4

@[simp]
theorem dens_map_equiv [Fintype β] (e : α ≃ β) : (s.map e.toEmbedding).dens = s.dens := by
  simp [dens, Fintype.card_congr e]

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

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

Разделы

Аффилиация

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