sdiff_nonempty_of_card_lt_card

Mathlib.Data.Finset.Card

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

← MathLib Explorer

English

If |s| < |t|, then t \ s is nonempty.

Русский

Если |s| < |t|, то t \ s непусто.

LaTeX

$$#s < #t ⇒ (t \ s).Nonempty$$

Lean4

theorem sdiff_nonempty_of_card_lt_card (h : #s < #t) : (t \ s).Nonempty :=
  by
  rw [nonempty_iff_ne_empty, Ne, sdiff_eq_empty_iff_subset]
  exact fun h' ↦ h.not_ge (card_le_card h')

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

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

Разделы

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

Аффилиация

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