ite_empty_right

Mathlib.Order.BooleanAlgebra.Set

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

English

For sets t and s, t.ite s ∅ equals s ∩ t.

Русский

Для множеств t и s выражение t.ite s ∅ равно s ∩ t.

LaTeX

$$$ t.\text{ite } s \emptyset = s \cap t $$$

Lean4

@[simp]
theorem ite_empty_right (t s : Set α) : t.ite s ∅ = s ∩ t := by simp [Set.ite]

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

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

Разделы

Аффилиация

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