dens_strictMono

Mathlib.Data.Finset.Density

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

English

The density function is strictly monotone with respect to strict inclusion.

Русский

Плотность строго монотонна при строгом включении.

LaTeX

$$$\\text{StrictMono}(\\mathrm{dens})$$$

Lean4

@[mono]
theorem dens_strictMono : StrictMono (dens : Finset α → ℚ≥0) := fun _ _ ↦ dens_lt_dens

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

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

Разделы

Аффилиация

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