encard_singleton_inter

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

The EN-cardinality of the intersection of a singleton with any set is at most 1.

Русский

Число encard пересечения множества с единичным множеством не превышает 1.

LaTeX

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

Lean4

theorem encard_singleton_inter (s : Set α) (x : α) : ({ x } ∩ s).encard ≤ 1 := by rw [← encard_singleton x];
  exact encard_le_encard inter_subset_left

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

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

Разделы

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

Аффилиация

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