symmDiff_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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