# Symmetric difference and bi-implication #

This file defines the symmetric difference and bi-implication operators in (co-)Heyting algebras.

## Examples #

Some examples are

- The symmetric difference of two sets is the set of elements that are in either but not both.
- The symmetric difference on propositions is `Xor'`.
- The symmetric difference on `Bool` is `Bool.xor`.
- The equivalence of propositions. Two propositions are equivalent if they imply each other.
- The symmetric difference translates to addition when considering a Boolean algebra as a Boolean ring.

## Main declarations #

- `symmDiff`: The symmetric difference operator, defined as `(a \ b) ⊔ (b \ a)`
- `bihimp`: The bi-implication operator, defined as `(b ⇨ a) ⊓ (a ⇨ b)`

In generalized Boolean algebras, the symmetric difference operator is:

- `symmDiff_comm`: commutative, and
- `symmDiff_assoc`: associative.

## Notation #

- `a ∆ b`: `symmDiff a b`
- `a ⇔ b`: `bihimp a b`

## References #

The proof of associativity follows the note "Associativity of the Symmetric Difference of Sets: A Proof from the Book" by John McCuan:

- https://people.math.gatech.edu/~mccuan/courses/4317/symmetricdifference.pdf

## Tags #

boolean ring, generalized boolean algebra, boolean algebra, symmetric difference, bi-implication, Heyting

source
def symmDiff {α : Type u_2} [Max α] [SDiff α] (a b : α) :
α

The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`.

Equations

- symmDiff a b = a \ b ⊔ b \ a

Instances For

source
def bihimp {α : Type u_2} [Min α] [HImp α] (a b : α) :
α

The Heyting bi-implication is `(b ⇨ a) ⊓ (a ⇨ b)`. This generalizes equivalence of propositions.

Equations

- bihimp a b = (b ⇨ a) ⊓ (a ⇨ b)

Instances For

source
def symmDiff.«term_∆_» :
Lean.TrailingParserDescr

Notation for symmDiff

Equations

- symmDiff.«term_∆_» = Lean.ParserDescr.trailingNode `symmDiff.«term_∆_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∆ ") (Lean.ParserDescr.cat `term 101))

Instances For

source
def symmDiff.«term_⇔_» :
Lean.TrailingParserDescr

Notation for bihimp

Equations

- symmDiff.«term_⇔_» = Lean.ParserDescr.trailingNode `symmDiff.«term_⇔_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇔ ") (Lean.ParserDescr.cat `term 101))

Instances For

source
theorem symmDiff_def {α : Type u_2} [Max α] [SDiff α] (a b : α) :
symmDiff a b = a \ b ⊔ b \ a
source
theorem bihimp_def {α : Type u_2} [Min α] [HImp α] (a b : α) :
bihimp a b = (b ⇨ a) ⊓ (a ⇨ b)
source
theorem symmDiff_eq_Xor' (p q : Prop) :
symmDiff p q = Xor' p q
source
@[simp]
theorem bihimp_iff_iff {p q : Prop} :
bihimp p q ↔ (p ↔ q)
source
@[simp]
theorem Bool.symmDiff_eq_xor (p q : Bool) :
symmDiff p q = (p ^^ q)
source
@[simp]
theorem toDual_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
OrderDual.toDual (symmDiff a b) = bihimp (OrderDual.toDual a) (OrderDual.toDual b)
source
@[simp]
theorem ofDual_bihimp {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α ᵒᵈ) :
OrderDual.ofDual (bihimp a b) = symmDiff (OrderDual.ofDual a) (OrderDual.ofDual b)
source
theorem symmDiff_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff a b = symmDiff b a
source
instance symmDiff_isCommutative {α : Type u_2} [GeneralizedCoheytingAlgebra α] :
Std.Commutative fun (x1 x2 : α) => symmDiff x1 x2
source
@[simp]
theorem symmDiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
symmDiff a a = ⊥
source
@[simp]
theorem symmDiff_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
symmDiff a ⊥ = a
source
@[simp]
theorem bot_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
symmDiff ⊥ a = a
source
@[simp]
theorem symmDiff_eq_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} :
symmDiff a b = ⊥ ↔ a = b
source
theorem symmDiff_of_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : a ≤ b) :
symmDiff a b = b \ a
source
theorem symmDiff_of_ge {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : b ≤ a) :
symmDiff a b = a \ b
source
theorem symmDiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) :
symmDiff a b ≤ c
source
theorem symmDiff_le_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} :
symmDiff a b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
source
@[simp]
theorem symmDiff_le_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} :
symmDiff a b ≤ a ⊔ b
source
theorem symmDiff_eq_sup_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff a b = (a ⊔ b) \ (a ⊓ b)
source
theorem Disjoint.symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : Disjoint a b) :
symmDiff a b = a ⊔ b
source
theorem symmDiff_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b c : α) :
symmDiff a b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
source
@[simp]
theorem symmDiff_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff a b \ (a ⊓ b) = symmDiff a b
source
@[simp]
theorem symmDiff_sdiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff a (b \ a) = a ⊔ b
source
@[simp]
theorem sdiff_symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff (a \ b) b = a ⊔ b
source
@[simp]
theorem symmDiff_sup_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff a b ⊔ a ⊓ b = a ⊔ b
source
@[simp]
theorem inf_sup_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
a ⊓ b ⊔ symmDiff a b = a ⊔ b
source
@[simp]
theorem symmDiff_symmDiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff (symmDiff a b) (a ⊓ b) = a ⊔ b
source
@[simp]
theorem inf_symmDiff_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
symmDiff (a ⊓ b) (symmDiff a b) = a ⊔ b
source
theorem symmDiff_triangle {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b c : α) :
symmDiff a c ≤ symmDiff a b ⊔ symmDiff b c
source
theorem le_symmDiff_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
a ≤ symmDiff a b ⊔ b
source
theorem le_symmDiff_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
b ≤ symmDiff a b ⊔ a
source
@[simp]
theorem toDual_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
OrderDual.toDual (bihimp a b) = symmDiff (OrderDual.toDual a) (OrderDual.toDual b)
source
@[simp]
theorem ofDual_symmDiff {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α ᵒᵈ) :
OrderDual.ofDual (symmDiff a b) = bihimp (OrderDual.ofDual a) (OrderDual.ofDual b)
source
theorem bihimp_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp a b = bihimp b a
source
instance bihimp_isCommutative {α : Type u_2} [GeneralizedHeytingAlgebra α] :
Std.Commutative fun (x1 x2 : α) => bihimp x1 x2
source
@[simp]
theorem bihimp_self {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
bihimp a a = ⊤
source
@[simp]
theorem bihimp_top {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
bihimp a ⊤ = a
source
@[simp]
theorem top_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
bihimp ⊤ a = a
source
@[simp]
theorem bihimp_eq_top {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} :
bihimp a b = ⊤ ↔ a = b
source
theorem bihimp_of_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : a ≤ b) :
bihimp a b = b ⇨ a
source
theorem bihimp_of_ge {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : b ≤ a) :
bihimp a b = a ⇨ b
source
theorem le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) :
a ≤ bihimp b c
source
theorem le_bihimp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} :
a ≤ bihimp b c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
source
@[simp]
theorem inf_le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} :
a ⊓ b ≤ bihimp a b
source
theorem bihimp_eq_sup_himp_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp a b = a ⊔ b ⇨ a ⊓ b
source
@[deprecated bihimp_eq_sup_himp_inf (since := "2025-06-05")]
theorem bihimp_eq_inf_himp_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp a b = a ⊔ b ⇨ a ⊓ b

Alias of `bihimp_eq_sup_himp_inf`.

source
theorem Codisjoint.bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) :
bihimp a b = a ⊓ b
source
theorem himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) :
a ⇨ bihimp b c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
source
@[simp]
theorem sup_himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
a ⊔ b ⇨ bihimp a b = bihimp a b
source
@[simp]
theorem bihimp_himp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp a (a ⇨ b) = a ⊓ b
source
@[simp]
theorem himp_bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp (b ⇨ a) b = a ⊓ b
source
@[simp]
theorem bihimp_inf_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp a b ⊓ (a ⊔ b) = a ⊓ b
source
@[simp]
theorem sup_inf_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
(a ⊔ b) ⊓ bihimp a b = a ⊓ b
source
@[simp]
theorem bihimp_bihimp_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp (bihimp a b) (a ⊔ b) = a ⊓ b
source
@[simp]
theorem sup_bihimp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
bihimp (a ⊔ b) (bihimp a b) = a ⊓ b
source
theorem bihimp_triangle {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) :
bihimp a b ⊓ bihimp b c ≤ bihimp a c
source
@[simp]
theorem symmDiff_top' {α : Type u_2} [CoheytingAlgebra α] (a : α) :
symmDiff a ⊤ = ￢a
source
@[simp]
theorem top_symmDiff' {α : Type u_2} [CoheytingAlgebra α] (a : α) :
symmDiff ⊤ a = ￢a
source
@[simp]
theorem hnot_symmDiff_self {α : Type u_2} [CoheytingAlgebra α] (a : α) :
symmDiff (￢a) a = ⊤
source
@[simp]
theorem symmDiff_hnot_self {α : Type u_2} [CoheytingAlgebra α] (a : α) :
symmDiff a (￢a) = ⊤
source
theorem IsCompl.symmDiff_eq_top {α : Type u_2} [CoheytingAlgebra α] {a b : α} (h : IsCompl a b) :
symmDiff a b = ⊤
source
@[simp]
theorem bihimp_bot {α : Type u_2} [HeytingAlgebra α] (a : α) :
bihimp a ⊥ = a ᶜ
source
@[simp]
theorem bot_bihimp {α : Type u_2} [HeytingAlgebra α] (a : α) :
bihimp ⊥ a = a ᶜ
source
@[simp]
theorem compl_bihimp_self {α : Type u_2} [HeytingAlgebra α] (a : α) :
bihimp a ᶜ a = ⊥
source
@[simp]
theorem bihimp_hnot_self {α : Type u_2} [HeytingAlgebra α] (a : α) :
bihimp a a ᶜ = ⊥
source
theorem IsCompl.bihimp_eq_bot {α : Type u_2} [HeytingAlgebra α] {a b : α} (h : IsCompl a b) :
bihimp a b = ⊥
source
@[simp]
theorem sup_sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
(a ⊔ b) \ symmDiff a b = a ⊓ b
source
theorem disjoint_symmDiff_inf {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
Disjoint (symmDiff a b) (a ⊓ b)
source
theorem inf_symmDiff_distrib_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
a ⊓ symmDiff b c = symmDiff (a ⊓ b) (a ⊓ c)
source
theorem inf_symmDiff_distrib_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff a b ⊓ c = symmDiff (a ⊓ c) (b ⊓ c)
source
theorem sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
c \ symmDiff a b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
source
theorem sdiff_symmDiff' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
c \ symmDiff a b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
source
@[simp]
theorem symmDiff_sdiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff a b \ a = b \ a
source
@[simp]
theorem symmDiff_sdiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff a b \ b = a \ b
source
@[simp]
theorem sdiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
a \ symmDiff a b = a ⊓ b
source
@[simp]
theorem sdiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
b \ symmDiff a b = a ⊓ b
source
theorem symmDiff_eq_sup {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff a b = a ⊔ b ↔ Disjoint a b
source
@[simp]
theorem le_symmDiff_iff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
a ≤ symmDiff a b ↔ Disjoint a b
source
@[simp]
theorem le_symmDiff_iff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
b ≤ symmDiff a b ↔ Disjoint a b
source
theorem symmDiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff (symmDiff a b) c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
source
theorem symmDiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff a (symmDiff b c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
source
theorem symmDiff_assoc {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff (symmDiff a b) c = symmDiff a (symmDiff b c)
source
instance symmDiff_isAssociative {α : Type u_2} [GeneralizedBooleanAlgebra α] :
Std.Associative fun (x1 x2 : α) => symmDiff x1 x2
source
theorem symmDiff_left_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff a (symmDiff b c) = symmDiff b (symmDiff a c)
source
theorem symmDiff_right_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
symmDiff (symmDiff a b) c = symmDiff (symmDiff a c) b
source
theorem symmDiff_symmDiff_symmDiff_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c d : α) :
symmDiff (symmDiff a b) (symmDiff c d) = symmDiff (symmDiff a c) (symmDiff b d)
source
@[simp]
theorem symmDiff_symmDiff_cancel_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff a (symmDiff a b) = b
source
@[simp]
theorem symmDiff_symmDiff_cancel_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff (symmDiff b a) a = b
source
@[simp]
theorem symmDiff_symmDiff_self' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
symmDiff (symmDiff a b) a = b
source
theorem symmDiff_left_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Involutive fun (x : α) => symmDiff x a
source
theorem symmDiff_right_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Involutive fun (x : α) => symmDiff a x
source
theorem symmDiff_left_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Injective fun (x : α) => symmDiff x a
source
theorem symmDiff_right_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Injective fun (x : α) => symmDiff a x
source
theorem symmDiff_left_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Surjective fun (x : α) => symmDiff x a
source
theorem symmDiff_right_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
Function.Surjective fun (x : α) => symmDiff a x
source
@[simp]
theorem symmDiff_left_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} :
symmDiff a b = symmDiff c b ↔ a = c
source
@[simp]
theorem symmDiff_right_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} :
symmDiff a b = symmDiff a c ↔ b = c
source
@[simp]
theorem symmDiff_eq_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} :
symmDiff a b = a ↔ b = ⊥
source
@[simp]
theorem symmDiff_eq_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} :
symmDiff a b = b ↔ a = ⊥
source
theorem Disjoint.symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
Disjoint (symmDiff a b) c
source
theorem Disjoint.symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} (ha : Disjoint a b) (hb : Disjoint a c) :
Disjoint a (symmDiff b c)
source
theorem symmDiff_eq_iff_sdiff_eq {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} (ha : a ≤ c) :
symmDiff a b = c ↔ c \ a = b

`CogeneralizedBooleanAlgebra` isn't actually a typeclass, but the lemmas in here are dual to the `GeneralizedBooleanAlgebra` ones

source
@[simp]
theorem inf_himp_bihimp {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b ⇨ a ⊓ b = a ⊔ b
source
theorem codisjoint_bihimp_sup {α : Type u_2} [BooleanAlgebra α] (a b : α) :
Codisjoint (bihimp a b) (a ⊔ b)
source
@[simp]
theorem himp_bihimp_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
a ⇨ bihimp a b = a ⇨ b
source
@[simp]
theorem himp_bihimp_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
b ⇨ bihimp a b = b ⇨ a
source
@[simp]
theorem bihimp_himp_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b ⇨ a = a ⊔ b
source
@[simp]
theorem bihimp_himp_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b ⇨ b = a ⊔ b
source
@[simp]
theorem bihimp_eq_inf {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b = a ⊓ b ↔ Codisjoint a b
source
@[simp]
theorem bihimp_le_iff_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b ≤ a ↔ Codisjoint a b
source
@[simp]
theorem bihimp_le_iff_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b ≤ b ↔ Codisjoint a b
source
theorem bihimp_assoc {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
bihimp (bihimp a b) c = bihimp a (bihimp b c)
source
instance bihimp_isAssociative {α : Type u_2} [BooleanAlgebra α] :
Std.Associative fun (x1 x2 : α) => bihimp x1 x2
source
theorem bihimp_left_comm {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
bihimp a (bihimp b c) = bihimp b (bihimp a c)
source
theorem bihimp_right_comm {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
bihimp (bihimp a b) c = bihimp (bihimp a c) b
source
theorem bihimp_bihimp_bihimp_comm {α : Type u_2} [BooleanAlgebra α] (a b c d : α) :
bihimp (bihimp a b) (bihimp c d) = bihimp (bihimp a c) (bihimp b d)
source
@[simp]
theorem bihimp_bihimp_cancel_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a (bihimp a b) = b
source
@[simp]
theorem bihimp_bihimp_cancel_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp (bihimp b a) a = b
source
@[simp]
theorem bihimp_bihimp_self {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp (bihimp a b) a = b
source
theorem bihimp_left_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Involutive fun (x : α) => bihimp x a
source
theorem bihimp_right_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Involutive fun (x : α) => bihimp a x
source
theorem bihimp_left_injective {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Injective fun (x : α) => bihimp x a
source
theorem bihimp_right_injective {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Injective fun (x : α) => bihimp a x
source
theorem bihimp_left_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Surjective fun (x : α) => bihimp x a
source
theorem bihimp_right_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) :
Function.Surjective fun (x : α) => bihimp a x
source
@[simp]
theorem bihimp_left_inj {α : Type u_2} [BooleanAlgebra α] {a b c : α} :
bihimp a b = bihimp c b ↔ a = c
source
@[simp]
theorem bihimp_right_inj {α : Type u_2} [BooleanAlgebra α] {a b c : α} :
bihimp a b = bihimp a c ↔ b = c
source
@[simp]
theorem bihimp_eq_left {α : Type u_2} [BooleanAlgebra α] {a b : α} :
bihimp a b = a ↔ b = ⊤
source
@[simp]
theorem bihimp_eq_right {α : Type u_2} [BooleanAlgebra α] {a b : α} :
bihimp a b = b ↔ a = ⊤
source
theorem Codisjoint.bihimp_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
Codisjoint (bihimp a b) c
source
theorem Codisjoint.bihimp_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (ha : Codisjoint a b) (hb : Codisjoint a c) :
Codisjoint a (bihimp b c)
source
theorem symmDiff_eq {α : Type u_2} [BooleanAlgebra α] (a b : α) :
symmDiff a b = a ⊓ b ᶜ ⊔ b ⊓ a ᶜ
source
theorem bihimp_eq {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b = (a ⊔ b ᶜ) ⊓ (b ⊔ a ᶜ)
source
theorem symmDiff_eq' {α : Type u_2} [BooleanAlgebra α] (a b : α) :
symmDiff a b = (a ⊔ b) ⊓ (a ᶜ ⊔ b ᶜ)
source
theorem bihimp_eq' {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b = a ⊓ b ⊔ a ᶜ ⊓ b ᶜ
source
theorem symmDiff_top {α : Type u_2} [BooleanAlgebra α] (a : α) :
symmDiff a ⊤ = a ᶜ
source
theorem top_symmDiff {α : Type u_2} [BooleanAlgebra α] (a : α) :
symmDiff ⊤ a = a ᶜ
source
@[simp]
theorem compl_symmDiff {α : Type u_2} [BooleanAlgebra α] (a b : α) :
(symmDiff a b)ᶜ = bihimp a b
source
@[simp]
theorem compl_bihimp {α : Type u_2} [BooleanAlgebra α] (a b : α) :
(bihimp a b)ᶜ = symmDiff a b
source
@[simp]
theorem compl_symmDiff_compl {α : Type u_2} [BooleanAlgebra α] (a b : α) :
symmDiff a ᶜ b ᶜ = symmDiff a b
source
@[simp]
theorem compl_bihimp_compl {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a ᶜ b ᶜ = bihimp a b
source
@[simp]
theorem symmDiff_eq_top {α : Type u_2} [BooleanAlgebra α] (a b : α) :
symmDiff a b = ⊤ ↔ IsCompl a b
source
@[simp]
theorem bihimp_eq_bot {α : Type u_2} [BooleanAlgebra α] (a b : α) :
bihimp a b = ⊥ ↔ IsCompl a b
source
@[simp]
theorem compl_symmDiff_self {α : Type u_2} [BooleanAlgebra α] (a : α) :
symmDiff a ᶜ a = ⊤
source
@[simp]
theorem symmDiff_compl_self {α : Type u_2} [BooleanAlgebra α] (a : α) :
symmDiff a a ᶜ = ⊤
source
theorem symmDiff_symmDiff_right' {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
symmDiff a (symmDiff b c) = a ⊓ b ⊓ c ⊔ a ⊓ b ᶜ ⊓ c ᶜ ⊔ a ᶜ ⊓ b ⊓ c ᶜ ⊔ a ᶜ ⊓ b ᶜ ⊓ c
source
theorem Disjoint.le_symmDiff_sup_symmDiff_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Disjoint a b) :
c ≤ symmDiff a c ⊔ symmDiff b c
source
theorem Disjoint.le_symmDiff_sup_symmDiff_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Disjoint b c) :
a ≤ symmDiff a b ⊔ symmDiff a c
source
theorem Codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Codisjoint a b) :
bihimp a c ⊓ bihimp b c ≤ c
source
theorem Codisjoint.bihimp_inf_bihimp_le_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Codisjoint b c) :
bihimp a b ⊓ bihimp a c ≤ a

### Prod #

source
@[simp]
theorem symmDiff_fst {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) :
(symmDiff a b).fst = symmDiff a.fst b.fst
source
@[simp]
theorem symmDiff_snd {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) :
(symmDiff a b).snd = symmDiff a.snd b.snd
source
@[simp]
theorem bihimp_fst {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) :
(bihimp a b).fst = bihimp a.fst b.fst
source
@[simp]
theorem bihimp_snd {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) :
(bihimp a b).snd = bihimp a.snd b.snd

### Pi #

source
theorem Pi.symmDiff_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedCoheytingAlgebra (π i)] (a b : (i : ι) → π i) :
symmDiff a b = fun (i : ι) => symmDiff (a i) (b i)
source
theorem Pi.bihimp_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedHeytingAlgebra (π i)] (a b : (i : ι) → π i) :
bihimp a b = fun (i : ι) => bihimp (a i) (b i)
source
@[simp]
theorem Pi.symmDiff_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedCoheytingAlgebra (π i)] (a b : (i : ι) → π i) (i : ι) :
symmDiff a b i = symmDiff (a i) (b i)
source
@[simp]
theorem Pi.bihimp_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedHeytingAlgebra (π i)] (a b : (i : ι) → π i) (i : ι) :
bihimp a b i = bihimp (a i) (b i)