toDual_symmDiff — Mathlib

English

Under order dual, the dual of a symmetric difference relates to a logical equivalence.

Русский

В двойственном порядке двойственная симметрическая разность связана с логической эквивалентностью.

LaTeX

$$$\\\\forall a,b \\\\in α, \\\\text{toDual}(a \\\\Delta b) \\\\Longleftrightarrow (\\\\text{toDual}a \\\\Leftrightarrow \\\\text{toDual}b)$$$

Lean4

@[simp]
theorem toDual_symmDiff : toDual (a ∆ b) = toDual a ⇔ toDual b :=
  rfl

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