sdiff_eq_sdiff_iff_inter_eq_inter

English

For any finite sets s,t1,t2, s \ t1 = s \ t2 if and only if s ∩ t1 = s ∩ t2.

Русский

Для любых конечных множеств s,t1,t2 верно: s \ t1 = s \ t2 тогда и только тогда, когда s ∩ t1 = s ∩ t2.

LaTeX

$$$ (s \ t_1) = (s \ t_2) \iff (s \cap t_1) = (s \cap t_2) $$$

Lean4

theorem sdiff_eq_sdiff_iff_inter_eq_inter {s t₁ t₂ : Finset α} : s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂ :=
  sdiff_eq_sdiff_iff_inf_eq_inf

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