card_singleton_inter

Mathlib.Data.Finset.Card

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

English

For any Finset s and element a, #({a} ∩ s) ≤ 1.

Русский

Для любого Finset s и элемента a, #( {a} ∩ s ) ≤ 1.

LaTeX

$$$\#\{a\} \cap s \le 1$$$

Lean4

theorem card_singleton_inter [DecidableEq α] : #({ a } ∩ s) ≤ 1 := by grind

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

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

Разделы

Аффилиация

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