encard_le_encard_iff_encard_diff_le_encard_diff

English

With (S ∩ T) finite, encard(S) ≤ encard(T) iff encard(S \ T) ≤ encard(T \ S).

Русский

При конечном пересечении S и T, encard(S) ≤ encard(T) тогда и только тогда, когда encard(S \ T) ≤ encard(T \ S).

LaTeX

$$$ (S \cap T).Finite \Rightarrow (S.encard \le T.encard \iff (S \setminus T).encard \le (T \setminus S).encard)$$$

Lean4

theorem encard_le_encard_iff_encard_diff_le_encard_diff (h : (s ∩ t).Finite) :
    s.encard ≤ t.encard ↔ (s \ t).encard ≤ (t \ s).encard := by
  rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
    WithTop.add_le_add_iff_right h.encard_lt_top.ne]

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