encard_pair

Mathlib.Data.Set.Card

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

← MathLib Explorer

English

If x ≠ y, then the encard of {x, y} equals 2.

Русский

Если x ≠ y, то encard({x, y}) = 2.

LaTeX

$$$(x \\neq y) \\Rightarrow encard({x,y}) = 2$$$

Lean4

theorem encard_pair {x y : α} (hne : x ≠ y) : ({ x, y } : Set α).encard = 2 := by
  rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two, WithTop.add_right_inj WithTop.one_ne_top,
    encard_singleton]

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

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

Разделы

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

Аффилиация

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