sdiff_subset_sdiff_iff_subset — Mathlib

English

For hs : s ⊆ r and ht : t ⊆ r, r \\ s ⊆ r \\ t iff t ⊆ s.

Русский

Пусть hs : s ⊆ r и ht : t ⊆ r; тогда r \\ s ⊆ r \\ t эквивалентно t ⊆ s.

LaTeX

$$$ (hs : s \\subseteq r) (ht : t \\subseteq r) : (r \\setminus s) \\subseteq (r \\setminus t) \\iff t \\subseteq s. $$$

Lean4

theorem sdiff_subset_sdiff_iff_subset {r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) : r \ s ⊆ r \ t ↔ t ⊆ s := by
  simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht

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