English
Under the same hypotheses, encard difference inequality holds between B1 \ B2 and B2 \ B1.
Русский
При тех же предпосылках неравенство encard между B1 \ B2 и B2 \ B1 выполняется.
LaTeX
$$$$ (B_1 \ B_2).encard \le (B_2 \ B_1).encard $$$$
Lean4
theorem encard_diff_le_aux {B₁ B₂ : Set α} (exch : ExchangeProperty IsBase) (hB₁ : IsBase B₁) (hB₂ : IsBase B₂) :
(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard :=
by
obtain (he | hinf | ⟨e, he, hcard⟩) := (B₂ \ B₁).eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
· rw [exch.antichain hB₂ hB₁ (diff_eq_empty.mp he)]
· exact le_top.trans_eq hinf.symm
obtain ⟨f, hf, hB'⟩ := exch B₂ B₁ hB₂ hB₁ e he
have : encard (insert f (B₂ \ { e }) \ B₁) < encard (B₂ \ B₁) := by rw [insert_diff_of_mem _ hf.1, diff_diff_comm];
exact hcard
have hencard := encard_diff_le_aux exch hB₁ hB'
rw [insert_diff_of_mem _ hf.1, diff_diff_comm, ← union_singleton, ← diff_diff, diff_diff_right,
inter_singleton_eq_empty.mpr he.2, union_empty] at hencard
rw [← encard_diff_singleton_add_one he, ← encard_diff_singleton_add_one hf]
exact add_le_add_right hencard 1
termination_by (B₂ \ B₁).encard
