ite_eq_of_subset_right

Mathlib.Order.BooleanAlgebra.Set

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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