ite_inter_inter — Mathlib

English

For all α, t, s1, s2, s1', s2' the equality t.ite (s1 ∩ s2) (s1' ∩ s2') = (t.ite s1 s1') ∩ (t.ite s2 s2').

Русский

Для любых α, t, s1, s2, s1', s2' выполняется тождество: t.ite (s1 ∩ s2) (s1' ∩ s2') = (t.ite s1 s1') ∩ (t.ite s2 s2').

LaTeX

$$$$ t.ite(s_1 \cap s_2)(s_1' \cap s_2') = (t.ite s_1 s_1') \cap (t.ite s_2 s_2'). $$$$

Lean4

theorem ite_inter_inter (t s₁ s₂ s₁' s₂' : Set α) : t.ite (s₁ ∩ s₂) (s₁' ∩ s₂') = t.ite s₁ s₁' ∩ t.ite s₂ s₂' :=
  by
  ext x
  simp only [Set.ite, Set.mem_inter_iff, Set.mem_diff, Set.mem_union]
  tauto

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