mk_compl_eq_mk_compl_infinite — Mathlib

English

If hs and ht express that two subsets s,t of a common infinite α have cardinalities less than α, then the complements s^c and t^c have equal cardinalities.

Русский

Если подмножества s и t бесконечного α имеют Кардинальность меньше α, то их дополнения имеют равную кардинальность.

LaTeX

$$$\\#s < \\#\\alpha \\rightarrow \\#t < \\#\\alpha \\rightarrow \\#(s^{c}) = \\#(t^{c})$$$

Lean4

theorem mk_compl_eq_mk_compl_infinite {α : Type*} [Infinite α] {s t : Set α} (hs : #s < #α) (ht : #t < #α) :
    #(sᶜ : Set α) = #(tᶜ : Set α) := by rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]

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