inter_subset_ite

Mathlib.Order.BooleanAlgebra.Set

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

English

The intersection s ∩ s' is contained in t.ite s s'.

Русский

Пересечение s ∩ s' содержится в t.ite s s'.

LaTeX

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

Lean4

theorem inter_subset_ite (t s s' : Set α) : s ∩ s' ⊆ t.ite s s' :=
  ite_same t (s ∩ s') ▸ ite_mono _ inter_subset_left inter_subset_right

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

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

Разделы

Аффилиация

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