mk_compl_eq_mk_compl_finite — Mathlib

English

If α is finite and β has the same cardinality as α, then the complements of equal-sized subsets also have the same cardinality.

Русский

Если α конечный и β имеет такую же кардинальность, то дополнения равных по размеру подмножеств имеют одинаковую кардинальность.

LaTeX

$$$\\#\\alpha = \\#\\beta \\Rightarrow \\#s^{c} = \\#t^{c}$$$

Lean4

theorem mk_compl_eq_mk_compl_finite {α β : Type u} [Finite α] {s : Set α} {t : Set β} (h1 : #α = #β) (h : #s = #t) :
    #(sᶜ : Set α) = #(tᶜ : Set β) := by
  rw [← lift_inj.{u, u}]
  apply mk_compl_eq_mk_compl_finite_lift.{u, u, u} <;> rwa [lift_inj]

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