disjoint_of_subset_right

Mathlib.Data.Multiset.UnionInter

URI: https://scilib.ai/kg/mathlib#Multiset.disjoint_of_subset_right

English

If t ⊆ u and Disjoint s u, then Disjoint s t.

Русский

Если t ⊆ u и Disjoint s u, то Disjoint s t.

LaTeX

$$$ (t \\subseteq u) \\land \\mathrm{Disjoint}(s, u) \\Rightarrow \\mathrm{Disjoint}(s, t) $$$

Lean4

theorem disjoint_of_subset_right {s t u : Multiset α} (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t :=
  (disjoint_of_subset_left h d.symm).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru