subset_left_of_subset_union

Mathlib.Data.Set.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.subset_left_of_subset_union

English

If s is a subset of t ∪ u and s is disjoint from u, then s ⊆ t.

Русский

Если s ⊆ t ∪ u и s несовместимо с u, то s ⊆ t.

LaTeX

$$$s \\subseteq (t \\cup u) \\Rightarrow (Disjoint\\ s\\ u) \\Rightarrow s \\subseteq t$$$

Lean4

theorem subset_left_of_subset_union (h : s ⊆ t ∪ u) (hac : Disjoint s u) : s ⊆ t :=
  hac.left_le_of_le_sup_right h

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

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

Разделы

Аффилиация

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