exists_mem_notMem_of_card_lt_card

Mathlib.Data.Finset.Card

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

← MathLib Explorer

English

If |s| < |t|, there exists e in t that is not in s.

Русский

Если |s| < |t|, существует элемент e в t, который не принадлежит s.

LaTeX

$$|s| < |t| ⇒ ∃ e ∈ t, e ∉ s$$

Lean4

theorem exists_mem_notMem_of_card_lt_card (h : #s < #t) : ∃ e, e ∈ t ∧ e ∉ s := by
  classical simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h

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

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

Разделы

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

Аффилиация

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