encard_lt_encard_iff_encard_diff_lt_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 < T.encard \iff (S \setminus T).encard < (T \setminus S).encard)$$$

Lean4

theorem encard_lt_encard_iff_encard_diff_lt_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_lt_add_iff_right h.encard_lt_top.ne]

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