some_sdiff_some — Mathlib

English

Let α be a type with a symmetric difference operation, and let a,b ∈ α. The embedding a ↦ some a preserves the operation, i.e. some a \ some b = some (a \ b).

Русский

Пусть α — тип с операцией симметрической разности, и возьмём a, b ∈ α. Встраивание a ↦ some a сохраняет операцию: some a \ some b = some (a \ b).

LaTeX

$$$$ \\operatorname{some}(a) \\backslash \\operatorname{some}(b) = \\operatorname{some}(a \\backslash b) $$$$

Lean4

theorem some_sdiff_some [SDiff α] (a b : α) : some a \ some b = some (a \ b) := by simp [sdiff_def]

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