union_subset_iff

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.union_subset_iff

English

s ∪ t ⊆ u iff s ⊆ u and t ⊆ u.

Русский

s ∪ t ⊆ u эквивалентно s ⊆ u и t ⊆ u.

LaTeX

$$$s \cup t \subseteq u \iff (s \subseteq u) \land (t \subseteq u)$$$

Lean4

@[simp]
theorem union_subset_iff {s t u : Set α} : s ∪ t ⊆ u ↔ s ⊆ u ∧ t ⊆ u :=
  (forall_congr' fun _ => or_imp).trans forall_and

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

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

Разделы

Аффилиация

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