encard_lt_top

Mathlib.Data.Set.Card

URI: https://scilib.ai/kg/mathlib#Set.Finite.encard_lt_top

← MathLib Explorer

English

If s is finite, then s.encard < ⊤.

Русский

Если s конечно, то s.encard < ⊤.

LaTeX

$$$ \text{Finite}(s) \Rightarrow s.encard < \top $$$

Lean4

theorem encard_lt_top (h : s.Finite) : s.encard < ⊤ := by
  induction s, h using Set.Finite.induction_on with
  | empty => simp
  | insert hat _ ht' =>
    rw [encard_insert_of_notMem hat]
    exact lt_tsub_iff_right.1 ht'

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

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

Разделы

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

Аффилиация

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