ite_inter_self

Mathlib.Order.BooleanAlgebra.Set

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

← MathLib Explorer

English

Suppose t is a set; then t.ite s s' intersect t equals s ∩ t.

Русский

Пусть t — множество; тогда (t.ite s s') ∩ t = s ∩ t.

LaTeX

$$$$ (t.ite s s') \cap t = s \cap t. $$$$

Lean4

@[simp]
theorem ite_inter_self (t s s' : Set α) : t.ite s s' ∩ t = s ∩ t := by
  rw [Set.ite, union_inter_distrib_right, diff_inter_self, inter_assoc, inter_self, union_empty]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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