pred_card_le_card_erase

Mathlib.Data.Finset.Card

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

English

The size decreases by at most 1 when erasing an element: #s − 1 ≤ #(s.erase a).

Русский

Размер уменьшается не более чем на единицу при стирании элемента: #s − 1 ≤ #(s.erase a).

LaTeX

$$$#s - 1 \le #(s.erase a)$$$

Lean4

theorem pred_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind

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

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

Разделы

Аффилиация

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