ite_eq_of_subset_left

Mathlib.Order.BooleanAlgebra.Set

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

← MathLib Explorer

English

If s1 ⊆ s2, then t.ite s1 s2 = s1 ∪ (s2 \ t).

Русский

Если s1 ⊆ s2, то t.ite s1 s2 = s1 ∪ (s2 \ t).

LaTeX

$$$ s_1 \subseteq s_2 \rightarrow t.ite s_1 s_2 = s_1 \cup (s_2 \ t) $$$

Lean4

theorem ite_eq_of_subset_left (t : Set α) {s₁ s₂ : Set α} (h : s₁ ⊆ s₂) : t.ite s₁ s₂ = s₁ ∪ (s₂ \ t) :=
  by
  ext x
  by_cases hx : x ∈ t <;> simp [*, Set.ite, or_iff_right_of_imp (@h x)]

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

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

Разделы

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

Аффилиация

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