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.

Notations

• 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

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

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

Equations

• a ∆ b = a \ b ⊔ b \ a

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

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

Equations

• a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)

def «term_∆_» : Lean.TrailingParserDescr

Notation for symmDiff

Equations

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

def «term_⇔_» : Lean.TrailingParserDescr

Notation for bihimp

Equations

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

theorem symmDiff_def {α : Type u_2} [Sup α] [SDiff α] (a : α) (b : α) : a ∆ b = a \ b ⊔ b \ a

theorem bihimp_def {α : Type u_2} [Inf α] [HImp α] (a : α) (b : α) : a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)

theorem symmDiff_eq_Xor' (p : Prop) (q : Prop) : p ∆ q = Xor' p q

@[simp]

theorem bihimp_iff_iff {p : Prop} {q : Prop} : p ⇔ q ↔ (p ↔ q)

@[simp]

theorem Bool.symmDiff_eq_xor (p : Bool) (q : Bool) : p ∆ q = xor p q

@[simp]

theorem toDual_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : ↑OrderDual.toDual (a ∆ b) = ↑OrderDual.toDual a ⇔ ↑OrderDual.toDual b

@[simp]

theorem ofDual_bihimp {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a ⇔ b) = ↑OrderDual.ofDual a ∆ ↑OrderDual.ofDual b

theorem symmDiff_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ b = b ∆ a

instance symmDiff_isCommutative {α : Type u_2} [GeneralizedCoheytingAlgebra α] : IsCommutative α fun x x_1 => x ∆ x_1

Equations

• @symmDiff_isCommutative = @symmDiff_isCommutative.proof_1

@[simp]

theorem symmDiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : a ∆ a = ⊥

@[simp]

theorem symmDiff_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : a ∆ ⊥ = a

@[simp]

theorem bot_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) : ⊥ ∆ a = a

@[simp]

theorem symmDiff_eq_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ∆ b = ⊥ ↔ a = b

theorem symmDiff_of_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : a ∆ b = b \ a

theorem symmDiff_of_ge {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : b ≤ a) : a ∆ b = a \ b

theorem symmDiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ∆ b ≤ c

theorem symmDiff_le_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} {c : α} : a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

@[simp]

theorem symmDiff_le_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} : a ∆ b ≤ a ⊔ b

theorem symmDiff_eq_sup_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ b = (a ⊔ b) \ (a ⊓ b)

theorem Disjoint.symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} {b : α} (h : Disjoint a b) : a ∆ b = a ⊔ b

theorem symmDiff_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

@[simp]

theorem symmDiff_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ b \ (a ⊓ b) = a ∆ b

@[simp]

theorem symmDiff_sdiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ (b \ a) = a ⊔ b

@[simp]

theorem sdiff_symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : (a \ b) ∆ b = a ⊔ b

@[simp]

theorem symmDiff_sup_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ b ⊔ a ⊓ b = a ⊔ b

@[simp]

theorem inf_sup_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ⊓ b ⊔ a ∆ b = a ⊔ b

@[simp]

theorem symmDiff_symmDiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : a ∆ b ∆ (a ⊓ b) = a ⊔ b

@[simp]

theorem inf_symmDiff_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

theorem symmDiff_triangle {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) (b : α) (c : α) : a ∆ c ≤ a ∆ b ⊔ b ∆ c

@[simp]

theorem toDual_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : ↑OrderDual.toDual (a ⇔ b) = ↑OrderDual.toDual a ∆ ↑OrderDual.toDual b

@[simp]

theorem ofDual_symmDiff {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : αᵒᵈ) (b : αᵒᵈ) : ↑OrderDual.ofDual (a ∆ b) = ↑OrderDual.ofDual a ⇔ ↑OrderDual.ofDual b

theorem bihimp_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⇔ b = b ⇔ a

instance bihimp_isCommutative {α : Type u_2} [GeneralizedHeytingAlgebra α] : IsCommutative α fun x x_1 => x ⇔ x_1

Equations

• @bihimp_isCommutative = @bihimp_isCommutative.proof_1

@[simp]

theorem bihimp_self {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : a ⇔ a = ⊤

@[simp]

theorem bihimp_top {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : a ⇔ ⊤ = a

@[simp]

theorem top_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) : ⊤ ⇔ a = a

@[simp]

theorem bihimp_eq_top {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ⇔ b = ⊤ ↔ a = b

theorem bihimp_of_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : a ≤ b) : a ⇔ b = b ⇨ a

theorem bihimp_of_ge {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : b ≤ a) : a ⇔ b = a ⇨ b

theorem le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) : a ≤ b ⇔ c

theorem le_bihimp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} {c : α} : a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b

@[simp]

theorem inf_le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} : a ⊓ b ≤ a ⇔ b

theorem bihimp_eq_inf_himp_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⇔ b = a ⊔ b ⇨ a ⊓ b

theorem Codisjoint.bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} {b : α} (h : Codisjoint a b) : a ⇔ b = a ⊓ b

theorem himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)

@[simp]

theorem sup_himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⊔ b ⇨ a ⇔ b = a ⇔ b

@[simp]

theorem bihimp_himp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⇔ (a ⇨ b) = a ⊓ b

@[simp]

theorem himp_bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : (b ⇨ a) ⇔ b = a ⊓ b

@[simp]

theorem bihimp_inf_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⇔ b ⊓ (a ⊔ b) = a ⊓ b

@[simp]

theorem sup_inf_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : (a ⊔ b) ⊓ a ⇔ b = a ⊓ b

@[simp]

theorem bihimp_bihimp_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : a ⇔ b ⇔ (a ⊔ b) = a ⊓ b

@[simp]

theorem sup_bihimp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) : (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b

theorem bihimp_triangle {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) (b : α) (c : α) : a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c

@[simp]

theorem symmDiff_top' {α : Type u_2} [CoheytingAlgebra α] (a : α) : a ∆ ⊤ = ￢a

@[simp]

theorem top_symmDiff' {α : Type u_2} [CoheytingAlgebra α] (a : α) : ⊤ ∆ a = ￢a

@[simp]

theorem hnot_symmDiff_self {α : Type u_2} [CoheytingAlgebra α] (a : α) : (￢a) ∆ a = ⊤

@[simp]

theorem symmDiff_hnot_self {α : Type u_2} [CoheytingAlgebra α] (a : α) : a ∆ (￢a) = ⊤

theorem IsCompl.symmDiff_eq_top {α : Type u_2} [CoheytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : a ∆ b = ⊤

@[simp]

theorem bihimp_bot {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇔ ⊥ = aᶜ

@[simp]

theorem bot_bihimp {α : Type u_2} [HeytingAlgebra α] (a : α) : ⊥ ⇔ a = aᶜ

@[simp]

theorem compl_bihimp_self {α : Type u_2} [HeytingAlgebra α] (a : α) : aᶜ ⇔ a = ⊥

@[simp]

theorem bihimp_hnot_self {α : Type u_2} [HeytingAlgebra α] (a : α) : a ⇔ aᶜ = ⊥

theorem IsCompl.bihimp_eq_bot {α : Type u_2} [HeytingAlgebra α] {a : α} {b : α} (h : IsCompl a b) : a ⇔ b = ⊥

@[simp]

theorem sup_sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : (a ⊔ b) \ a ∆ b = a ⊓ b

theorem disjoint_symmDiff_inf {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : Disjoint (a ∆ b) (a ⊓ b)

theorem inf_symmDiff_distrib_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)

theorem inf_symmDiff_distrib_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

theorem sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b

theorem sdiff_symmDiff' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

@[simp]

theorem symmDiff_sdiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ∆ b \ a = b \ a

@[simp]

theorem symmDiff_sdiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ∆ b \ b = a \ b

@[simp]

theorem sdiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a \ a ∆ b = a ⊓ b

@[simp]

theorem sdiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : b \ a ∆ b = a ⊓ b

theorem symmDiff_eq_sup {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ∆ b = a ⊔ b ↔ Disjoint a b

@[simp]

theorem le_symmDiff_iff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ≤ a ∆ b ↔ Disjoint a b

@[simp]

theorem le_symmDiff_iff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : b ≤ a ∆ b ↔ Disjoint a b

theorem symmDiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

theorem symmDiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

theorem symmDiff_assoc {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ b ∆ c = a ∆ (b ∆ c)

instance symmDiff_isAssociative {α : Type u_2} [GeneralizedBooleanAlgebra α] : IsAssociative α fun x x_1 => x ∆ x_1

Equations

• @symmDiff_isAssociative = @symmDiff_isAssociative.proof_1

theorem symmDiff_left_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ (b ∆ c) = b ∆ (a ∆ c)

theorem symmDiff_right_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ b ∆ c = a ∆ c ∆ b

theorem symmDiff_symmDiff_symmDiff_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) (d : α) : a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

@[simp]

theorem symmDiff_symmDiff_cancel_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ∆ (a ∆ b) = b

@[simp]

theorem symmDiff_symmDiff_cancel_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : b ∆ a ∆ a = b

@[simp]

theorem symmDiff_symmDiff_self' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) (b : α) : a ∆ b ∆ a = b

theorem symmDiff_left_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Involutive fun x => x ∆ a

theorem symmDiff_right_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Involutive ((fun x x_1 => x ∆ x_1) a)

theorem symmDiff_left_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Injective fun x => x ∆ a

theorem symmDiff_right_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Injective ((fun x x_1 => x ∆ x_1) a)

theorem symmDiff_left_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Surjective fun x => x ∆ a

theorem symmDiff_right_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) : Function.Surjective ((fun x x_1 => x ∆ x_1) a)

@[simp]

theorem symmDiff_left_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} {c : α} : a ∆ b = c ∆ b ↔ a = c

@[simp]

theorem symmDiff_right_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} {c : α} : a ∆ b = a ∆ c ↔ b = c

@[simp]

theorem symmDiff_eq_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : a ∆ b = a ↔ b = ⊥

@[simp]

theorem symmDiff_eq_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} : a ∆ b = b ↔ a = ⊥

theorem Disjoint.symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} {c : α} (ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ∆ b) c

theorem Disjoint.symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} {c : α} (ha : Disjoint a b) (hb : Disjoint a c) : Disjoint a (b ∆ c)

theorem symmDiff_eq_iff_sdiff_eq {α : Type u_2} [GeneralizedBooleanAlgebra α] {a : α} {b : α} {c : α} (ha : a ≤ c) : a ∆ b = c ↔ c \ a = b

@[simp]

theorem inf_himp_bihimp {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ⇨ a ⊓ b = a ⊔ b

theorem codisjoint_bihimp_sup {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : Codisjoint (a ⇔ b) (a ⊔ b)

@[simp]

theorem himp_bihimp_left {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇨ a ⇔ b = a ⇨ b

@[simp]

theorem himp_bihimp_right {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : b ⇨ a ⇔ b = b ⇨ a

@[simp]

theorem bihimp_himp_left {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ⇨ a = a ⊔ b

@[simp]

theorem bihimp_himp_right {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ⇨ b = a ⊔ b

@[simp]

theorem bihimp_eq_inf {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b = a ⊓ b ↔ Codisjoint a b

@[simp]

theorem bihimp_le_iff_left {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ≤ a ↔ Codisjoint a b

@[simp]

theorem bihimp_le_iff_right {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ≤ b ↔ Codisjoint a b

theorem bihimp_assoc {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) (c : α) : a ⇔ b ⇔ c = a ⇔ (b ⇔ c)

instance bihimp_isAssociative {α : Type u_2} [BooleanAlgebra α] : IsAssociative α fun x x_1 => x ⇔ x_1

Equations

• @bihimp_isAssociative = @bihimp_isAssociative.proof_1

theorem bihimp_left_comm {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) (c : α) : a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

theorem bihimp_right_comm {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) (c : α) : a ⇔ b ⇔ c = a ⇔ c ⇔ b

theorem bihimp_bihimp_bihimp_comm {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) (c : α) (d : α) : a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

@[simp]

theorem bihimp_bihimp_cancel_left {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ (a ⇔ b) = b

@[simp]

theorem bihimp_bihimp_cancel_right {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : b ⇔ a ⇔ a = b

@[simp]

theorem bihimp_bihimp_self {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b ⇔ a = b

theorem bihimp_left_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Involutive fun x => x ⇔ a

theorem bihimp_right_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Involutive ((fun x x_1 => x ⇔ x_1) a)

theorem bihimp_left_injective {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Injective fun x => x ⇔ a

theorem bihimp_right_injective {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Injective ((fun x x_1 => x ⇔ x_1) a)

theorem bihimp_left_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Surjective fun x => x ⇔ a

theorem bihimp_right_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) : Function.Surjective ((fun x x_1 => x ⇔ x_1) a)

@[simp]

theorem bihimp_left_inj {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} : a ⇔ b = c ⇔ b ↔ a = c

@[simp]

theorem bihimp_right_inj {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} : a ⇔ b = a ⇔ c ↔ b = c

@[simp]

theorem bihimp_eq_left {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} : a ⇔ b = a ↔ b = ⊤

@[simp]

theorem bihimp_eq_right {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} : a ⇔ b = b ↔ a = ⊤

theorem Codisjoint.bihimp_left {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) : Codisjoint (a ⇔ b) c

theorem Codisjoint.bihimp_right {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (ha : Codisjoint a b) (hb : Codisjoint a c) : Codisjoint a (b ⇔ c)

theorem symmDiff_eq {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

theorem bihimp_eq {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)

theorem symmDiff_eq' {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

theorem bihimp_eq' {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b = a ⊓ b ⊔ aᶜ ⊓ bᶜ

theorem symmDiff_top {α : Type u_2} [BooleanAlgebra α] (a : α) : a ∆ ⊤ = aᶜ

theorem top_symmDiff {α : Type u_2} [BooleanAlgebra α] (a : α) : ⊤ ∆ a = aᶜ

@[simp]

theorem compl_symmDiff {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : (a ∆ b)ᶜ = a ⇔ b

@[simp]

theorem compl_bihimp {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : (a ⇔ b)ᶜ = a ∆ b

@[simp]

theorem compl_symmDiff_compl {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : aᶜ ∆ bᶜ = a ∆ b

@[simp]

theorem compl_bihimp_compl {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : aᶜ ⇔ bᶜ = a ⇔ b

@[simp]

theorem symmDiff_eq_top {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ∆ b = ⊤ ↔ IsCompl a b

@[simp]

theorem bihimp_eq_bot {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) : a ⇔ b = ⊥ ↔ IsCompl a b

@[simp]

theorem compl_symmDiff_self {α : Type u_2} [BooleanAlgebra α] (a : α) : aᶜ ∆ a = ⊤

@[simp]

theorem symmDiff_compl_self {α : Type u_2} [BooleanAlgebra α] (a : α) : a ∆ aᶜ = ⊤

theorem symmDiff_symmDiff_right' {α : Type u_2} [BooleanAlgebra α] (a : α) (b : α) (c : α) : a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

theorem Disjoint.le_symmDiff_sup_symmDiff_left {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (h : Disjoint a b) : c ≤ a ∆ c ⊔ b ∆ c

theorem Disjoint.le_symmDiff_sup_symmDiff_right {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (h : Disjoint b c) : a ≤ a ∆ b ⊔ a ∆ c

theorem Codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (h : Codisjoint a b) : a ⇔ c ⊓ b ⇔ c ≤ c

theorem Codisjoint.bihimp_inf_bihimp_le_right {α : Type u_2} [BooleanAlgebra α] {a : α} {b : α} {c : α} (h : Codisjoint b c) : a ⇔ b ⊓ a ⇔ c ≤ a

Prod

@[simp]

theorem symmDiff_fst {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a : α × β) (b : α × β) : (a ∆ b).fst = a.fst ∆ b.fst

@[simp]

theorem symmDiff_snd {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a : α × β) (b : α × β) : (a ∆ b).snd = a.snd ∆ b.snd

@[simp]

theorem bihimp_fst {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a : α × β) (b : α × β) : (a ⇔ b).fst = a.fst ⇔ b.fst

@[simp]

theorem bihimp_snd {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a : α × β) (b : α × β) : (a ⇔ b).snd = a.snd ⇔ b.snd

Pi

theorem Pi.symmDiff_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedCoheytingAlgebra (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) : a ∆ b = fun i => a i ∆ b i

theorem Pi.bihimp_def {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedHeytingAlgebra (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) : a ⇔ b = fun i => a i ⇔ b i

@[simp]

theorem Pi.symmDiff_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedCoheytingAlgebra (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) : (((i : ι) → π i) ∆ Pi.instSupForAll) Pi.sdiff a b i = a i ∆ b i

@[simp]

theorem Pi.bihimp_apply {ι : Type u_1} {π : ι → Type u_4} [(i : ι) → GeneralizedHeytingAlgebra (π i)] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) : (((i : ι) → π i) ⇔ Pi.instInfForAll) Pi.instHImpForAll a b i = a i ⇔ b i