bot_symmDiff — Mathlib

English

Let α be a generalized coheyting algebra. Then the symmetric difference with the bottom element is the identity: ⊥ Δ a = a for all a ∈ α.

Русский

Пусть α — обобщённая когейтинговая алгебра. Тогда симметрическая разность с нижним элементом есть тождественный отображение: ⊥ Δ a = a для любого a ∈ α.

LaTeX

$$$$ \\bot \\Delta a = a $$$$

Lean4

@[simp]
theorem bot_symmDiff : ⊥ ∆ a = a := by rw [symmDiff_comm, symmDiff_bot]

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