disjoint_of_subset_right

Mathlib.Data.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#Set.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 \to \mathrm{Disjoint}(s,u) \to \mathrm{Disjoint}(s,t)$$$

Lean4

theorem disjoint_of_subset_right (h : t ⊆ u) (d : Disjoint s u) : Disjoint s t :=
  d.mono_right h

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

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

Разделы

Аффилиация

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