ite_inter_of_inter_eq

Mathlib.Order.BooleanAlgebra.Set

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

English

If s1 ∩ s = s2 ∩ s, then t.ite s1 s2 ∩ s = s1 ∩ s.

Русский

Если s1 ∩ s = s2 ∩ s, тогда t.ite s1 s2 ∩ s = s1 ∩ s.

LaTeX

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

Lean4

theorem ite_inter_of_inter_eq (t : Set α) {s₁ s₂ s : Set α} (h : s₁ ∩ s = s₂ ∩ s) : t.ite s₁ s₂ ∩ s = s₁ ∩ s := by
  rw [← ite_inter, ← h, ite_same]

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

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

Разделы

Аффилиация

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