ite_subset_union

Mathlib.Order.BooleanAlgebra.Set

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

English

The ITE expression is always a subset of the union of its two middle arguments: t.ite s s' ⊆ s ∪ s'.

Русский

Выражение ITE всегда является подмножеством объединения двух средних аргументов: t.ite s s' ⊆ s ∪ s'.

LaTeX

$$$$ t.ite s s' \subseteq s \cup s'. $$$$

Lean4

theorem ite_subset_union (t s s' : Set α) : t.ite s s' ⊆ s ∪ s' :=
  union_subset_union inter_subset_left diff_subset

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

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

Разделы

Аффилиация

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