mathlib3 documentation

order.symm_diff

Symmetric difference and bi-implication #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Examples #

Some examples are

Main declarations #

In generalized Boolean algebras, the symmetric difference operator is:

Notations #

References #

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

Tags #

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

source
def symm_diff {α : Type u_2} [has_sup α] [has_sdiff α] (a b : α) :
α

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

Equations
Instances for symm_diff
source
def bihimp {α : Type u_2} [has_inf α] [has_himp α] (a b : α) :
α

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

Equations
Instances for bihimp
source
theorem symm_diff_def {α : Type u_2} [has_sup α] [has_sdiff α] (a b : α) :
a ∆ b = a \ b ⊔ b \ a
source
theorem bihimp_def {α : Type u_2} [has_inf α] [has_himp α] (a b : α) :
a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)
source
theorem symm_diff_eq_xor (p q : Prop) :
p ∆ q = xor p q
source
@[simp]
theorem bihimp_iff_iff {p q : Prop} :
p ⇔ q ↔ (p ↔ q)
source
@[simp]
theorem bool.symm_diff_eq_bxor (p q : bool) :
p ∆ q = bxor p q
source
@[simp]
theorem to_dual_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
⇑order_dual.to_dual (a ∆ b) = ⇑order_dual.to_dual a ⇔ ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_bihimp {α : Type u_2} [generalized_coheyting_algebra α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a ⇔ b) = ⇑order_dual.of_dual a ∆ ⇑order_dual.of_dual b
source
theorem symm_diff_comm {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ b = b ∆ a
source
@[protected, instance]
def symm_diff_is_comm {α : Type u_2} [generalized_coheyting_algebra α] :
is_commutative α symm_diff
source
@[simp]
theorem symm_diff_self {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
a ∆ a = ⊥
source
@[simp]
theorem symm_diff_bot {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
a ∆ ⊥ = a
source
@[simp]
theorem bot_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
⊥ ∆ a = a
source
@[simp]
theorem symm_diff_eq_bot {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ∆ b = ⊥ ↔ a = b
source
theorem symm_diff_of_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : a ≤ b) :
a ∆ b = b \ a
source
theorem symm_diff_of_ge {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : b ≤ a) :
a ∆ b = a \ b
source
theorem symm_diff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) :
a ∆ b ≤ c
source
theorem symm_diff_le_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
source
@[simp]
theorem symm_diff_le_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a ∆ b ≤ a ⊔ b
source
theorem symm_diff_eq_sup_sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ b = (a ⊔ b) \ (a ⊓ b)
source
theorem disjoint.symm_diff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
a ∆ b = a ⊔ b
source
theorem symm_diff_sdiff {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
source
@[simp]
theorem symm_diff_sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ b \ (a ⊓ b) = a ∆ b
source
@[simp]
theorem symm_diff_sdiff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ (b \ a) = a ⊔ b
source
@[simp]
theorem sdiff_symm_diff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
(a \ b) ∆ b = a ⊔ b
source
@[simp]
theorem symm_diff_sup_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ b ⊔ a ⊓ b = a ⊔ b
source
@[simp]
theorem inf_sup_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ⊓ b ⊔ a ∆ b = a ⊔ b
source
@[simp]
theorem symm_diff_symm_diff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a ∆ b ∆ (a ⊓ b) = a ⊔ b
source
@[simp]
theorem inf_symm_diff_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
(a ⊓ b) ∆ (a ∆ b) = a ⊔ b
source
theorem symm_diff_triangle {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a ∆ c ≤ a ∆ b ⊔ b ∆ c
source
@[simp]
theorem to_dual_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
⇑order_dual.to_dual (a ⇔ b) = ⇑order_dual.to_dual a ∆ ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_symm_diff {α : Type u_2} [generalized_heyting_algebra α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a ∆ b) = ⇑order_dual.of_dual a ⇔ ⇑order_dual.of_dual b
source
theorem bihimp_comm {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⇔ b = b ⇔ a
source
@[protected, instance]
def bihimp_is_comm {α : Type u_2} [generalized_heyting_algebra α] :
is_commutative α bihimp
source
@[simp]
theorem bihimp_self {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
a ⇔ a = ⊤
source
@[simp]
theorem bihimp_top {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
a ⇔ ⊤ = a
source
@[simp]
theorem top_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
⊤ ⇔ a = a
source
@[simp]
theorem bihimp_eq_top {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ⇔ b = ⊤ ↔ a = b
source
theorem bihimp_of_le {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : a ≤ b) :
a ⇔ b = b ⇨ a
source
theorem bihimp_of_ge {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : b ≤ a) :
a ⇔ b = a ⇨ b
source
theorem le_bihimp {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) :
a ≤ b ⇔ c
source
theorem le_bihimp_iff {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
source
@[simp]
theorem inf_le_bihimp {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a ⊓ b ≤ a ⇔ b
source
theorem bihimp_eq_inf_himp_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⇔ b = a ⊔ b ⇨ a ⊓ b
source
theorem codisjoint.bihimp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a ⇔ b = a ⊓ b
source
theorem himp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
source
@[simp]
theorem sup_himp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⊔ b ⇨ a ⇔ b = a ⇔ b
source
@[simp]
theorem bihimp_himp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⇔ (a ⇨ b) = a ⊓ b
source
@[simp]
theorem himp_bihimp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(b ⇨ a) ⇔ b = a ⊓ b
source
@[simp]
theorem bihimp_inf_sup {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⇔ b ⊓ (a ⊔ b) = a ⊓ b
source
@[simp]
theorem sup_inf_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(a ⊔ b) ⊓ a ⇔ b = a ⊓ b
source
@[simp]
theorem bihimp_bihimp_sup {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a ⇔ b ⇔ (a ⊔ b) = a ⊓ b
source
@[simp]
theorem sup_bihimp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b
source
theorem bihimp_triangle {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c
source
@[simp]
theorem symm_diff_top' {α : Type u_2} [coheyting_algebra α] (a : α) :
a ∆ ⊤ = ￢a
source
@[simp]
theorem top_symm_diff' {α : Type u_2} [coheyting_algebra α] (a : α) :
⊤ ∆ a = ￢a
source
@[simp]
theorem hnot_symm_diff_self {α : Type u_2} [coheyting_algebra α] (a : α) :
(￢a) ∆ a = ⊤
source
@[simp]
theorem symm_diff_hnot_self {α : Type u_2} [coheyting_algebra α] (a : α) :
a ∆ ￢a = ⊤
source
theorem is_compl.symm_diff_eq_top {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
a ∆ b = ⊤
source
@[simp]
theorem bihimp_bot {α : Type u_2} [heyting_algebra α] (a : α) :
a ⇔ ⊥ = aᶜ
source
@[simp]
theorem bot_bihimp {α : Type u_2} [heyting_algebra α] (a : α) :
⊥ ⇔ a = aᶜ
source
@[simp]
theorem compl_bihimp_self {α : Type u_2} [heyting_algebra α] (a : α) :
aᶜ ⇔ a = ⊥
source
@[simp]
theorem bihimp_hnot_self {α : Type u_2} [heyting_algebra α] (a : α) :
a ⇔ aᶜ = ⊥
source
theorem is_compl.bihimp_eq_bot {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
a ⇔ b = ⊥
source
@[simp]
theorem sup_sdiff_symm_diff {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
(a ⊔ b) \ a ∆ b = a ⊓ b
source
theorem disjoint_symm_diff_inf {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
disjoint (a ∆ b) (a ⊓ b)
source
theorem inf_symm_diff_distrib_left {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
source
theorem inf_symm_diff_distrib_right {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
source
theorem sdiff_symm_diff {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
source
theorem sdiff_symm_diff' {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
source
@[simp]
theorem symm_diff_sdiff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ∆ b \ a = b \ a
source
@[simp]
theorem symm_diff_sdiff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ∆ b \ b = a \ b
source
@[simp]
theorem sdiff_symm_diff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a \ a ∆ b = a ⊓ b
source
@[simp]
theorem sdiff_symm_diff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b \ a ∆ b = a ⊓ b
source
theorem symm_diff_eq_sup {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ∆ b = a ⊔ b ↔ disjoint a b
source
@[simp]
theorem le_symm_diff_iff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ≤ a ∆ b ↔ disjoint a b
source
@[simp]
theorem le_symm_diff_iff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b ≤ a ∆ b ↔ disjoint a b
source
theorem symm_diff_symm_diff_left {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
source
theorem symm_diff_symm_diff_right {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
source
theorem symm_diff_assoc {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ b ∆ c = a ∆ (b ∆ c)
source
@[protected, instance]
def symm_diff_is_assoc {α : Type u_2} [generalized_boolean_algebra α] :
is_associative α symm_diff
source
theorem symm_diff_left_comm {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ (b ∆ c) = b ∆ (a ∆ c)
source
theorem symm_diff_right_comm {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a ∆ b ∆ c = a ∆ c ∆ b
source
theorem symm_diff_symm_diff_symm_diff_comm {α : Type u_2} [generalized_boolean_algebra α] (a b c d : α) :
a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
source
@[simp]
theorem symm_diff_symm_diff_cancel_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ∆ (a ∆ b) = b
source
@[simp]
theorem symm_diff_symm_diff_cancel_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b ∆ a ∆ a = b
source
@[simp]
theorem symm_diff_symm_diff_self' {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a ∆ b ∆ a = b
source
theorem symm_diff_left_involutive {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.involutive (λ (_x : α), _x ∆ a)
source
theorem symm_diff_right_involutive {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.involutive (symm_diff a)
source
theorem symm_diff_left_injective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.injective (λ (_x : α), _x ∆ a)
source
theorem symm_diff_right_injective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.injective (symm_diff a)
source
theorem symm_diff_left_surjective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.surjective (λ (_x : α), _x ∆ a)
source
theorem symm_diff_right_surjective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.surjective (symm_diff a)
source
@[simp]
theorem symm_diff_left_inj {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} :
a ∆ b = c ∆ b ↔ a = c
source
@[simp]
theorem symm_diff_right_inj {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} :
a ∆ b = a ∆ c ↔ b = c
source
@[simp]
theorem symm_diff_eq_left {α : Type u_2} [generalized_boolean_algebra α] {a b : α} :
a ∆ b = a ↔ b = ⊥
source
@[simp]
theorem symm_diff_eq_right {α : Type u_2} [generalized_boolean_algebra α] {a b : α} :
a ∆ b = b ↔ a = ⊥
source
@[protected]
theorem disjoint.symm_diff_left {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
disjoint (a ∆ b) c
source
@[protected]
theorem disjoint.symm_diff_right {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} (ha : disjoint a b) (hb : disjoint a c) :
disjoint a (b ∆ c)
source
theorem symm_diff_eq_iff_sdiff_eq {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} (ha : a ≤ c) :
a ∆ b = c ↔ c \ a = b
source
@[simp]
theorem inf_himp_bihimp {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ⇨ a ⊓ b = a ⊔ b
source
theorem codisjoint_bihimp_sup {α : Type u_2} [boolean_algebra α] (a b : α) :
codisjoint (a ⇔ b) (a ⊔ b)
source
@[simp]
theorem himp_bihimp_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇨ a ⇔ b = a ⇨ b
source
@[simp]
theorem himp_bihimp_right {α : Type u_2} [boolean_algebra α] (a b : α) :
b ⇨ a ⇔ b = b ⇨ a
source
@[simp]
theorem bihimp_himp_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ⇨ a = a ⊔ b
source
@[simp]
theorem bihimp_himp_right {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ⇨ b = a ⊔ b
source
@[simp]
theorem bihimp_eq_inf {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b = a ⊓ b ↔ codisjoint a b
source
@[simp]
theorem bihimp_le_iff_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ≤ a ↔ codisjoint a b
source
@[simp]
theorem bihimp_le_iff_right {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ≤ b ↔ codisjoint a b
source
theorem bihimp_assoc {α : Type u_2} [boolean_algebra α] (a b c : α) :
a ⇔ b ⇔ c = a ⇔ (b ⇔ c)
source
@[protected, instance]
def bihimp_is_assoc {α : Type u_2} [boolean_algebra α] :
is_associative α bihimp
source
theorem bihimp_left_comm {α : Type u_2} [boolean_algebra α] (a b c : α) :
a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
source
theorem bihimp_right_comm {α : Type u_2} [boolean_algebra α] (a b c : α) :
a ⇔ b ⇔ c = a ⇔ c ⇔ b
source
theorem bihimp_bihimp_bihimp_comm {α : Type u_2} [boolean_algebra α] (a b c d : α) :
a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
source
@[simp]
theorem bihimp_bihimp_cancel_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ (a ⇔ b) = b
source
@[simp]
theorem bihimp_bihimp_cancel_right {α : Type u_2} [boolean_algebra α] (a b : α) :
b ⇔ a ⇔ a = b
source
@[simp]
theorem bihimp_bihimp_self {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b ⇔ a = b
source
theorem bihimp_left_involutive {α : Type u_2} [boolean_algebra α] (a : α) :
function.involutive (λ (_x : α), _x ⇔ a)
source
theorem bihimp_right_involutive {α : Type u_2} [boolean_algebra α] (a : α) :
function.involutive (bihimp a)
source
theorem bihimp_left_injective {α : Type u_2} [boolean_algebra α] (a : α) :
function.injective (λ (_x : α), _x ⇔ a)
source
theorem bihimp_right_injective {α : Type u_2} [boolean_algebra α] (a : α) :
function.injective (bihimp a)
source
theorem bihimp_left_surjective {α : Type u_2} [boolean_algebra α] (a : α) :
function.surjective (λ (_x : α), _x ⇔ a)
source
theorem bihimp_right_surjective {α : Type u_2} [boolean_algebra α] (a : α) :
function.surjective (bihimp a)
source
@[simp]
theorem bihimp_left_inj {α : Type u_2} [boolean_algebra α] {a b c : α} :
a ⇔ b = c ⇔ b ↔ a = c
source
@[simp]
theorem bihimp_right_inj {α : Type u_2} [boolean_algebra α] {a b c : α} :
a ⇔ b = a ⇔ c ↔ b = c
source
@[simp]
theorem bihimp_eq_left {α : Type u_2} [boolean_algebra α] {a b : α} :
a ⇔ b = a ↔ b = ⊤
source
@[simp]
theorem bihimp_eq_right {α : Type u_2} [boolean_algebra α] {a b : α} :
a ⇔ b = b ↔ a = ⊤
source
@[protected]
theorem codisjoint.bihimp_left {α : Type u_2} [boolean_algebra α] {a b c : α} (ha : codisjoint a c) (hb : codisjoint b c) :
codisjoint (a ⇔ b) c
source
@[protected]
theorem codisjoint.bihimp_right {α : Type u_2} [boolean_algebra α] {a b c : α} (ha : codisjoint a b) (hb : codisjoint a c) :
codisjoint a (b ⇔ c)
source
theorem symm_diff_eq {α : Type u_2} [boolean_algebra α] (a b : α) :
a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ
source
theorem bihimp_eq {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)
source
theorem symm_diff_eq' {α : Type u_2} [boolean_algebra α] (a b : α) :
a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
source
theorem bihimp_eq' {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b = a ⊓ b ⊔ aᶜ ⊓ bᶜ
source
theorem symm_diff_top {α : Type u_2} [boolean_algebra α] (a : α) :
a ∆ ⊤ = aᶜ
source
theorem top_symm_diff {α : Type u_2} [boolean_algebra α] (a : α) :
⊤ ∆ a = aᶜ
source
@[simp]
theorem compl_symm_diff {α : Type u_2} [boolean_algebra α] (a b : α) :
(a ∆ b)ᶜ = a ⇔ b
source
@[simp]
theorem compl_bihimp {α : Type u_2} [boolean_algebra α] (a b : α) :
(a ⇔ b)ᶜ = a ∆ b
source
@[simp]
theorem compl_symm_diff_compl {α : Type u_2} [boolean_algebra α] (a b : α) :
aᶜ ∆ bᶜ = a ∆ b
source
@[simp]
theorem compl_bihimp_compl {α : Type u_2} [boolean_algebra α] (a b : α) :
aᶜ ⇔ bᶜ = a ⇔ b
source
@[simp]
theorem symm_diff_eq_top {α : Type u_2} [boolean_algebra α] (a b : α) :
a ∆ b = ⊤ ↔ is_compl a b
source
@[simp]
theorem bihimp_eq_bot {α : Type u_2} [boolean_algebra α] (a b : α) :
a ⇔ b = ⊥ ↔ is_compl a b
source
@[simp]
theorem compl_symm_diff_self {α : Type u_2} [boolean_algebra α] (a : α) :
aᶜ ∆ a = ⊤
source
@[simp]
theorem symm_diff_compl_self {α : Type u_2} [boolean_algebra α] (a : α) :
a ∆ aᶜ = ⊤
source
theorem symm_diff_symm_diff_right' {α : Type u_2} [boolean_algebra α] (a b c : α) :
a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
source
theorem disjoint.le_symm_diff_sup_symm_diff_left {α : Type u_2} [boolean_algebra α] {a b c : α} (h : disjoint a b) :
c ≤ a ∆ c ⊔ b ∆ c
source
theorem disjoint.le_symm_diff_sup_symm_diff_right {α : Type u_2} [boolean_algebra α] {a b c : α} (h : disjoint b c) :
a ≤ a ∆ b ⊔ a ∆ c
source
theorem codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [boolean_algebra α] {a b c : α} (h : codisjoint a b) :
a ⇔ c ⊓ b ⇔ c ≤ c
source
theorem codisjoint.bihimp_inf_bihimp_le_right {α : Type u_2} [boolean_algebra α] {a b c : α} (h : codisjoint b c) :
a ⇔ b ⊓ a ⇔ c ≤ a

Prod #

source
@[simp]
theorem symm_diff_fst {α : Type u_2} {β : Type u_3} [generalized_coheyting_algebra α] [generalized_coheyting_algebra β] (a b : α × β) :
(a ∆ b).fst = a.fst ∆ b.fst
source
@[simp]
theorem symm_diff_snd {α : Type u_2} {β : Type u_3} [generalized_coheyting_algebra α] [generalized_coheyting_algebra β] (a b : α × β) :
(a ∆ b).snd = a.snd ∆ b.snd
source
@[simp]
theorem bihimp_fst {α : Type u_2} {β : Type u_3} [generalized_heyting_algebra α] [generalized_heyting_algebra β] (a b : α × β) :
(a ⇔ b).fst = a.fst ⇔ b.fst
source
@[simp]
theorem bihimp_snd {α : Type u_2} {β : Type u_3} [generalized_heyting_algebra α] [generalized_heyting_algebra β] (a b : α × β) :
(a ⇔ b).snd = a.snd ⇔ b.snd

Pi #

source
theorem pi.symm_diff_def {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), generalized_coheyting_algebra (π i)] (a b : Π (i : ι), π i) :
a ∆ b = λ (i : ι), a i ∆ b i
source
theorem pi.bihimp_def {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), generalized_heyting_algebra (π i)] (a b : Π (i : ι), π i) :
a ⇔ b = λ (i : ι), a i ⇔ b i
source
@[simp]
theorem pi.symm_diff_apply {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), generalized_coheyting_algebra (π i)] (a b : Π (i : ι), π i) (i : ι) :
(a ∆ b) i = a i ∆ b i
source
@[simp]
theorem pi.bihimp_apply {ι : Type u_1} {π : ι → Type u_4} [Π (i : ι), generalized_heyting_algebra (π i)] (a b : Π (i : ι), π i) (i : ι) :
(a ⇔ b) i = a i ⇔ b i