ite_inter

Mathlib.Order.BooleanAlgebra.Set

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

English

Let t, s1, s2, s be subsets of a type α. Then t.ite (s1 ∩ s) (s2 ∩ s) = (t.ite s1 s2) ∩ s.

Русский

Пусть t, s1, s2, s — подмножества множества α. Тогда t.ite (s1 ∩ s) (s2 ∩ s) = (t.ite s1 s2) ∩ s.

LaTeX

$$$ t.ite (s_1 \cap s) (s_2 \cap s) = (t.ite s_1 s_2) \cap s $$$

Lean4

theorem ite_inter (t s₁ s₂ s : Set α) : t.ite (s₁ ∩ s) (s₂ ∩ s) = t.ite s₁ s₂ ∩ s := by rw [ite_inter_inter, ite_same]

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

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

Разделы

Аффилиация

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