ncard_pair

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

If a ≠ b, the set {a,b} has cardinality 2.

Русский

Если a ≠ b, кардинал набора {a,b} равен 2.

LaTeX

$$$ \text{If } a \neq b,\n(\{a,b\} : Set \alpha).ncard = 2 $$$

Lean4

theorem ncard_pair {a b : α} (h : a ≠ b) : ({ a, b } : Set α).ncard = 2 := by
  simp [h]
    -- removing `@[simp]` because the LHS is not in simp normal form

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

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

Разделы

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

Аффилиация

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