English
If α and β are finite with equal cardinalities and s ⊆ α, t ⊆ β have equal cardinalities, then the lifted complements have equal cardinalities.
Русский
Если конечные множества α и β имеют одинаковую кардинальность, и подмножества s ⊆ α, t ⊆ β имеют равные кардинальности, то их дополнения после подъема по лифту имеют равную кардинальность.
LaTeX
$$$\\#\\alpha = \\#\\beta \\;\\wedge\\; \\#s = \\#t \\Rightarrow \\#(s^{c}) = #(t^{c})$$$
Lean4
theorem mk_compl_eq_mk_compl_finite_lift {α : Type u} {β : Type v} [Finite α] {s : Set α} {t : Set β}
(h1 : (lift.{max v w, u} #α) = (lift.{max u w, v} #β)) (h2 : lift.{max v w, u} #s = lift.{max u w, v} #t) :
lift.{max v w} #(sᶜ : Set α) = lift.{max u w} #(tᶜ : Set β) :=
by
cases nonempty_fintype α
rcases lift_mk_eq.{u, v, w}.1 h1 with ⟨e⟩; letI : Fintype β := Fintype.ofEquiv α e
replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
classical
lift s to Finset α using s.toFinite
lift t to Finset β using t.toFinite
simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl, lift_natCast, h1, h2]
