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

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
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
theorem symm_diff_def {α : Type u_2} [has_sup α] [has_sdiff α] (a b : α) :
a b = a \ b b \ a
theorem bihimp_def {α : Type u_2} [has_inf α] [has_himp α] (a b : α) :
a b = (b a) (a b)
theorem symm_diff_eq_xor (p q : Prop) :
p q = xor p q
@[simp]
theorem bihimp_iff_iff {p q : Prop} :
p q (p q)
@[simp]
theorem bool.symm_diff_eq_bxor (p q : bool) :
p q = bxor p q
theorem symm_diff_comm {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b = b a
@[protected, instance]
@[simp]
theorem symm_diff_self {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
a a =
@[simp]
theorem symm_diff_bot {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
a = a
@[simp]
theorem bot_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a : α) :
a = a
@[simp]
theorem symm_diff_eq_bot {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a b = a = b
theorem symm_diff_of_le {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : a b) :
a b = b \ a
theorem symm_diff_of_ge {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : b a) :
a b = a \ b
theorem symm_diff_le {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} (ha : a b c) (hb : b a c) :
a b c
theorem symm_diff_le_iff {α : Type u_2} [generalized_coheyting_algebra α] {a b c : α} :
a b c a b c b a c
@[simp]
theorem symm_diff_le_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} :
a b a b
theorem symm_diff_eq_sup_sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b = (a b) \ (a b)
theorem disjoint.symm_diff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] {a b : α} (h : disjoint a b) :
a b = a b
theorem symm_diff_sdiff {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a b \ c = a \ (b c) b \ (a c)
@[simp]
theorem symm_diff_sdiff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b \ (a b) = a b
@[simp]
theorem symm_diff_sdiff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a (b \ a) = a b
@[simp]
theorem sdiff_symm_diff_eq_sup {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
(a \ b) b = a b
@[simp]
theorem symm_diff_sup_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b a b = a b
@[simp]
theorem inf_sup_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b a b = a b
@[simp]
theorem symm_diff_symm_diff_inf {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
a b (a b) = a b
@[simp]
theorem inf_symm_diff_symm_diff {α : Type u_2} [generalized_coheyting_algebra α] (a b : α) :
(a b) (a b) = a b
theorem symm_diff_triangle {α : Type u_2} [generalized_coheyting_algebra α] (a b c : α) :
a c a b b c
theorem bihimp_comm {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b = b a
@[protected, instance]
@[simp]
theorem bihimp_self {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
a a =
@[simp]
theorem bihimp_top {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
a = a
@[simp]
theorem top_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a : α) :
a = a
@[simp]
theorem bihimp_eq_top {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a b = a = b
theorem bihimp_of_le {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : a b) :
a b = b a
theorem bihimp_of_ge {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : b a) :
a b = a b
theorem le_bihimp {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} (hb : a b c) (hc : a c b) :
a b c
theorem le_bihimp_iff {α : Type u_2} [generalized_heyting_algebra α] {a b c : α} :
a b c a b c a c b
@[simp]
theorem inf_le_bihimp {α : Type u_2} [generalized_heyting_algebra α] {a b : α} :
a b a b
theorem bihimp_eq_inf_himp_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b = a b a b
theorem codisjoint.bihimp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] {a b : α} (h : codisjoint a b) :
a b = a b
theorem himp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b c = (a c b) (a b c)
@[simp]
theorem sup_himp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b a b = a b
@[simp]
theorem bihimp_himp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a (a b) = a b
@[simp]
theorem himp_bihimp_eq_inf {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(b a) b = a b
@[simp]
theorem bihimp_inf_sup {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b (a b) = a b
@[simp]
theorem sup_inf_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(a b) a b = a b
@[simp]
theorem bihimp_bihimp_sup {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
a b (a b) = a b
@[simp]
theorem sup_bihimp_bihimp {α : Type u_2} [generalized_heyting_algebra α] (a b : α) :
(a b) (a b) = a b
theorem bihimp_triangle {α : Type u_2} [generalized_heyting_algebra α] (a b c : α) :
a b b c a c
@[simp]
theorem symm_diff_top' {α : Type u_2} [coheyting_algebra α] (a : α) :
@[simp]
theorem top_symm_diff' {α : Type u_2} [coheyting_algebra α] (a : α) :
@[simp]
theorem hnot_symm_diff_self {α : Type u_2} [coheyting_algebra α] (a : α) :
(a) a =
@[simp]
theorem symm_diff_hnot_self {α : Type u_2} [coheyting_algebra α] (a : α) :
theorem is_compl.symm_diff_eq_top {α : Type u_2} [coheyting_algebra α] {a b : α} (h : is_compl a b) :
a b =
@[simp]
theorem bihimp_bot {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem bot_bihimp {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem compl_bihimp_self {α : Type u_2} [heyting_algebra α] (a : α) :
@[simp]
theorem bihimp_hnot_self {α : Type u_2} [heyting_algebra α] (a : α) :
theorem is_compl.bihimp_eq_bot {α : Type u_2} [heyting_algebra α] {a b : α} (h : is_compl a b) :
a b =
@[simp]
theorem sup_sdiff_symm_diff {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
(a b) \ a b = a b
theorem disjoint_symm_diff_inf {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
disjoint (a b) (a b)
theorem inf_symm_diff_distrib_left {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a b c = (a b) (a c)
theorem inf_symm_diff_distrib_right {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a b c = (a c) (b c)
theorem sdiff_symm_diff {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
c \ a b = c a b c \ a c \ b
theorem sdiff_symm_diff' {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
c \ a b = c a b c \ (a b)
@[simp]
theorem symm_diff_sdiff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a b \ a = b \ a
@[simp]
theorem symm_diff_sdiff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a b \ b = a \ b
@[simp]
theorem sdiff_symm_diff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a \ a b = a b
@[simp]
theorem sdiff_symm_diff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b \ a b = a b
theorem symm_diff_eq_sup {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a b = a b disjoint a b
@[simp]
theorem le_symm_diff_iff_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a a b disjoint a b
@[simp]
theorem le_symm_diff_iff_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b a b disjoint a b
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
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
theorem symm_diff_assoc {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a b c = a (b c)
@[protected, instance]
theorem symm_diff_left_comm {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a (b c) = b (a c)
theorem symm_diff_right_comm {α : Type u_2} [generalized_boolean_algebra α] (a b c : α) :
a b c = a c b
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)
@[simp]
theorem symm_diff_symm_diff_cancel_left {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a (a b) = b
@[simp]
theorem symm_diff_symm_diff_cancel_right {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
b a a = b
@[simp]
theorem symm_diff_symm_diff_self' {α : Type u_2} [generalized_boolean_algebra α] (a b : α) :
a b a = b
theorem symm_diff_left_involutive {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.involutive (λ (_x : α), _x a)
theorem symm_diff_left_injective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.injective (λ (_x : α), _x a)
theorem symm_diff_left_surjective {α : Type u_2} [generalized_boolean_algebra α] (a : α) :
function.surjective (λ (_x : α), _x a)
@[simp]
theorem symm_diff_left_inj {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} :
a b = c b a = c
@[simp]
theorem symm_diff_right_inj {α : Type u_2} [generalized_boolean_algebra α] {a b c : α} :
a b = a c b = c
@[simp]
theorem symm_diff_eq_left {α : Type u_2} [generalized_boolean_algebra α] {a b : α} :
a b = a b =
@[simp]
theorem symm_diff_eq_right {α : Type u_2} [generalized_boolean_algebra α] {a b : α} :
a b = b a =
@[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
@[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)
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
@[simp]
theorem inf_himp_bihimp {α : Type u_2} [boolean_algebra α] (a b : α) :
a b a b = a b
theorem codisjoint_bihimp_sup {α : Type u_2} [boolean_algebra α] (a b : α) :
codisjoint (a b) (a b)
@[simp]
theorem himp_bihimp_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a a b = a b
@[simp]
theorem himp_bihimp_right {α : Type u_2} [boolean_algebra α] (a b : α) :
b a b = b a
@[simp]
theorem bihimp_himp_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a b a = a b
@[simp]
theorem bihimp_himp_right {α : Type u_2} [boolean_algebra α] (a b : α) :
a b b = a b
@[simp]
theorem bihimp_eq_inf {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = a b codisjoint a b
@[simp]
theorem bihimp_le_iff_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a b a codisjoint a b
@[simp]
theorem bihimp_le_iff_right {α : Type u_2} [boolean_algebra α] (a b : α) :
a b b codisjoint a b
theorem bihimp_assoc {α : Type u_2} [boolean_algebra α] (a b c : α) :
a b c = a (b c)
@[protected, instance]
theorem bihimp_left_comm {α : Type u_2} [boolean_algebra α] (a b c : α) :
a (b c) = b (a c)
theorem bihimp_right_comm {α : Type u_2} [boolean_algebra α] (a b c : α) :
a b c = a c b
theorem bihimp_bihimp_bihimp_comm {α : Type u_2} [boolean_algebra α] (a b c d : α) :
a b (c d) = a c (b d)
@[simp]
theorem bihimp_bihimp_cancel_left {α : Type u_2} [boolean_algebra α] (a b : α) :
a (a b) = b
@[simp]
theorem bihimp_bihimp_cancel_right {α : Type u_2} [boolean_algebra α] (a b : α) :
b a a = b
@[simp]
theorem bihimp_bihimp_self {α : Type u_2} [boolean_algebra α] (a b : α) :
a b a = b
theorem bihimp_left_involutive {α : Type u_2} [boolean_algebra α] (a : α) :
function.involutive (λ (_x : α), _x a)
theorem bihimp_left_injective {α : Type u_2} [boolean_algebra α] (a : α) :
function.injective (λ (_x : α), _x a)
theorem bihimp_left_surjective {α : Type u_2} [boolean_algebra α] (a : α) :
function.surjective (λ (_x : α), _x a)
@[simp]
theorem bihimp_left_inj {α : Type u_2} [boolean_algebra α] {a b c : α} :
a b = c b a = c
@[simp]
theorem bihimp_right_inj {α : Type u_2} [boolean_algebra α] {a b c : α} :
a b = a c b = c
@[simp]
theorem bihimp_eq_left {α : Type u_2} [boolean_algebra α] {a b : α} :
a b = a b =
@[simp]
theorem bihimp_eq_right {α : Type u_2} [boolean_algebra α] {a b : α} :
a b = b a =
@[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
@[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)
theorem symm_diff_eq {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = a b b a
theorem bihimp_eq {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = (a b) (b a)
theorem symm_diff_eq' {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = (a b) (a b)
theorem bihimp_eq' {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = a b a b
theorem symm_diff_top {α : Type u_2} [boolean_algebra α] (a : α) :
theorem top_symm_diff {α : Type u_2} [boolean_algebra α] (a : α) :
@[simp]
theorem compl_symm_diff {α : Type u_2} [boolean_algebra α] (a b : α) :
(a b) = a b
@[simp]
theorem compl_bihimp {α : Type u_2} [boolean_algebra α] (a b : α) :
(a b) = a b
@[simp]
theorem compl_symm_diff_compl {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = a b
@[simp]
theorem compl_bihimp_compl {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = a b
@[simp]
theorem symm_diff_eq_top {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = is_compl a b
@[simp]
theorem bihimp_eq_bot {α : Type u_2} [boolean_algebra α] (a b : α) :
a b = is_compl a b
@[simp]
theorem compl_symm_diff_self {α : Type u_2} [boolean_algebra α] (a : α) :
@[simp]
theorem symm_diff_compl_self {α : Type u_2} [boolean_algebra α] (a : α) :
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
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
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
theorem codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [boolean_algebra α] {a b c : α} (h : codisjoint a b) :
a c b c c
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 #

@[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
@[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
@[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
@[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 #

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
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
@[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
@[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