mk_compl_eq_mk_compl_finite_same

Mathlib.SetTheory.Cardinal.Arithmetic

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

← MathLib Explorer

English

If s and t are finite subsets of a finite α with |s| = |t|, then |s^c| = |t^c|.

Русский

Если s и t — конечные подмножества α, и |s| = |t|, то |s^c| = |t^c|.

LaTeX

$$$\\#s = \\#t \\Rightarrow \\#(s^{c}) = \\#(t^{c})$$$

Lean4

theorem mk_compl_eq_mk_compl_finite_same {α : Type u} [Finite α] {s t : Set α} (h : #s = #t) :
    #(sᶜ : Set α) = #(tᶜ : Set α) :=
  mk_compl_eq_mk_compl_finite.{u} rfl h

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

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

Разделы

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

Аффилиация

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