encard_tsub_one_le_encard_diff_singleton

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.encard_tsub_one_le_encard_diff_singleton

← MathLib Explorer

English

For any s and x, encard(s) − 1 ≤ encard(s \\ {x}).

Русский

Для любого s и x выполнено encard(s) − 1 ≤ encard(s \\ {x}).

LaTeX

$$$encard(s) - 1 \\le encard(s \\\\ {x})$$$

Lean4

theorem encard_tsub_one_le_encard_diff_singleton (s : Set α) (x : α) : s.encard - 1 ≤ (s \ { x }).encard := by
  rw [← encard_singleton x]; apply tsub_encard_le_encard_diff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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