union_subset_left

Mathlib.Data.Finset.Lattice.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem union_subset_left (h : s ∪ t ⊆ u) : s ⊆ u :=
  subset_union_left.trans h

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

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

Разделы

Аффилиация

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