mk_congr

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_congr

English

If α is equivalent to β, then their cardinalities are equal: #α = #β.

Русский

Если α эквивалентен β, то их кардинальности равны: #α = #β.

LaTeX

$$$\\forall \\alpha\\,\\beta\\, (e:\\\u2009\\alpha \\simeq \\beta),\\; \\#\\alpha = \\#\\beta$$$

Lean4

theorem mk_congr (e : α ≃ β) : #α = #β :=
  Quot.sound ⟨e⟩

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

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

Разделы

Аффилиация

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