symmDiff_snd — Mathlib

English

For a,b in products α×β, the second projection of their symmetric difference equals the symmetric difference of the second projections: (a Δ b).2 = a.2 Δ b.2.

Русский

Для пар (a,b) в произведении α×β вторая проекция симметрической разности равна симметрической разности вторых проекций: (a Δ b).2 = a.2 Δ b.2.

LaTeX

$$$ (a \triangle b).2 = a.2 \triangle b.2 $$$

Lean4

@[simp]
theorem symmDiff_snd [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) :
    (a ∆ b).2 = a.2 ∆ b.2 :=
  rfl

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