sigma_diff_sigma — Mathlib

English

The difference of two sigmas distributes as (s1.sigma t1 \\ s2.sigma t2) = s1.sigma (t1 \\ t2) ∪ (s1 \\ s2).sigma t1.

Русский

Разность двух сигм распадается как (s1.sigma t1 \\ s2.sigma t2) = s1.sigma (t1 \\ t2) ∪ (s1 \\ s2).sigma t1.

LaTeX

$$$ s_1 \\sigma t_1 \\setminus s_2 \\sigma t_2 \\\\ = \\; s_1 \\sigma (t_1 \\setminus t_2) \\; \\cup \\; (s_1 \\setminus s_2).\\sigma t_1 $$$

Lean4

theorem sigma_diff_sigma : s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁ :=
  ext fun x ↦ by by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1 <;> simp [*, ← imp_iff_or_not]

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