diff_subset_diff_iff_subset — Mathlib

English

Let r, s, t be sets with s ⊆ r and t ⊆ r. Then r \ s ⊆ r \ t iff t ⊆ s.

Русский

Пусть r, s, t — множества такие, что s ⊆ r и t ⊆ r. Тогда r \ s ⊆ r \ t ⇔ t ⊆ s.

LaTeX

$$$ (s \subseteq r) \land (t \subseteq r) \Rightarrow (r \setminus s \subseteq r \setminus t) \iff (t \subseteq s)$$$

Lean4

theorem diff_subset_diff_iff_subset {r : Set α} (hs : s ⊆ r) (ht : t ⊆ r) : r \ s ⊆ r \ t ↔ t ⊆ s :=
  sdiff_le_sdiff_iff_le hs ht

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