union_subset_right

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.union_subset_right

English

If S ∪ T ⊆ U, then T ⊆ U.

Русский

Если S ∪ T ⊆ U, то T ⊆ U.

LaTeX

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

Lean4

theorem union_subset_right {s t u : Finset α} (h : s ∪ t ⊆ u) : t ⊆ u :=
  Subset.trans subset_union_right h

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

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

Разделы

Аффилиация

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