encard_eq_encard_iff_encard_diff_eq_encard_diff

English

If (S ∩ T) is finite, then S.encard = T.encard iff (S \ T).encard = (T \ S).encard.

Русский

Если (S ∩ T) конечно, то S.encard = T.encard тогда и только тогда, когда (S \ T).encard = (T \ S).encard.

LaTeX

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

Lean4

theorem encard_eq_encard_iff_encard_diff_eq_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_right_inj h.encard_lt_top.ne]

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