Documentation

Mathlib.Order.SymmDiff

Symmetric difference and bi-implication #

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 symmDiff {α : Type u_2} [Max α] [SDiff α] (a b : α) :
α

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

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

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

      Equations
        Instances For

          Notation for symmDiff

          Equations
            Instances For

              Notation for bihimp

              Equations
                Instances For
                  theorem symmDiff_def {α : Type u_2} [Max α] [SDiff α] (a b : α) :
                  symmDiff a b = a \ bb \ a
                  theorem bihimp_def {α : Type u_2} [Min α] [HImp α] (a b : α) :
                  bihimp a b = (b a) ⊓ (a b)
                  theorem symmDiff_eq_Xor' (p q : Prop) :
                  symmDiff p q = Xor' p q
                  @[simp]
                  theorem bihimp_iff_iff {p q : Prop} :
                  bihimp p q (p q)
                  @[simp]
                  theorem Bool.symmDiff_eq_xor (p q : Bool) :
                  symmDiff p q = (p ^^ q)
                  theorem symmDiff_comm {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  instance symmDiff_isCommutative {α : Type u_2} [GeneralizedCoheytingAlgebra α] :
                  Std.Commutative fun (x1 x2 : α) => symmDiff x1 x2
                  @[simp]
                  theorem symmDiff_self {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem symmDiff_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem bot_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem symmDiff_eq_bot {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} :
                  symmDiff a b = a = b
                  theorem symmDiff_of_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : a b) :
                  symmDiff a b = b \ a
                  theorem symmDiff_of_ge {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : b a) :
                  symmDiff a b = a \ b
                  theorem symmDiff_le {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} (ha : a bc) (hb : b ac) :
                  theorem symmDiff_le_iff {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b c : α} :
                  symmDiff a b c a bc b ac
                  @[simp]
                  theorem symmDiff_le_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} :
                  symmDiff a b ab
                  theorem symmDiff_eq_sup_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff a b = (ab) \ (ab)
                  theorem Disjoint.symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a b : α} (h : Disjoint a b) :
                  symmDiff a b = ab
                  theorem symmDiff_sdiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b c : α) :
                  symmDiff a b \ c = a \ (bc)b \ (ac)
                  @[simp]
                  theorem symmDiff_sdiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff a b \ (ab) = symmDiff a b
                  @[simp]
                  theorem symmDiff_sdiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff a (b \ a) = ab
                  @[simp]
                  theorem sdiff_symmDiff_eq_sup {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff (a \ b) b = ab
                  @[simp]
                  theorem symmDiff_sup_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff a bab = ab
                  @[simp]
                  theorem inf_sup_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  absymmDiff a b = ab
                  @[simp]
                  theorem symmDiff_symmDiff_inf {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff (symmDiff a b) (ab) = ab
                  @[simp]
                  theorem inf_symmDiff_symmDiff {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  symmDiff (ab) (symmDiff a b) = ab
                  theorem symmDiff_triangle {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b c : α) :
                  symmDiff a c symmDiff a bsymmDiff b c
                  theorem le_symmDiff_sup_right {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  a symmDiff a bb
                  theorem le_symmDiff_sup_left {α : Type u_2} [GeneralizedCoheytingAlgebra α] (a b : α) :
                  b symmDiff a ba
                  theorem bihimp_comm {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp a b = bihimp b a
                  instance bihimp_isCommutative {α : Type u_2} [GeneralizedHeytingAlgebra α] :
                  Std.Commutative fun (x1 x2 : α) => bihimp x1 x2
                  @[simp]
                  theorem bihimp_self {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem bihimp_top {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem top_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem bihimp_eq_top {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} :
                  bihimp a b = a = b
                  theorem bihimp_of_le {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : a b) :
                  bihimp a b = b a
                  theorem bihimp_of_ge {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : b a) :
                  bihimp a b = a b
                  theorem le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} (hb : ab c) (hc : ac b) :
                  a bihimp b c
                  theorem le_bihimp_iff {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b c : α} :
                  a bihimp b c ab c ac b
                  @[simp]
                  theorem inf_le_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} :
                  ab bihimp a b
                  theorem bihimp_eq_inf_himp_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp a b = ab ab
                  theorem Codisjoint.bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] {a b : α} (h : Codisjoint a b) :
                  bihimp a b = ab
                  theorem himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) :
                  a bihimp b c = (ac b) ⊓ (ab c)
                  @[simp]
                  theorem sup_himp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  ab bihimp a b = bihimp a b
                  @[simp]
                  theorem bihimp_himp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp a (a b) = ab
                  @[simp]
                  theorem himp_bihimp_eq_inf {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp (b a) b = ab
                  @[simp]
                  theorem bihimp_inf_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp a b(ab) = ab
                  @[simp]
                  theorem sup_inf_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  (ab)bihimp a b = ab
                  @[simp]
                  theorem bihimp_bihimp_sup {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp (bihimp a b) (ab) = ab
                  @[simp]
                  theorem sup_bihimp_bihimp {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b : α) :
                  bihimp (ab) (bihimp a b) = ab
                  theorem bihimp_triangle {α : Type u_2} [GeneralizedHeytingAlgebra α] (a b c : α) :
                  bihimp a bbihimp b c bihimp a c
                  @[simp]
                  theorem symmDiff_top' {α : Type u_2} [CoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem top_symmDiff' {α : Type u_2} [CoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem hnot_symmDiff_self {α : Type u_2} [CoheytingAlgebra α] (a : α) :
                  @[simp]
                  theorem symmDiff_hnot_self {α : Type u_2} [CoheytingAlgebra α] (a : α) :
                  theorem IsCompl.symmDiff_eq_top {α : Type u_2} [CoheytingAlgebra α] {a b : α} (h : IsCompl a b) :
                  @[simp]
                  theorem bihimp_bot {α : Type u_2} [HeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem bot_bihimp {α : Type u_2} [HeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem compl_bihimp_self {α : Type u_2} [HeytingAlgebra α] (a : α) :
                  @[simp]
                  theorem bihimp_hnot_self {α : Type u_2} [HeytingAlgebra α] (a : α) :
                  theorem IsCompl.bihimp_eq_bot {α : Type u_2} [HeytingAlgebra α] {a b : α} (h : IsCompl a b) :
                  @[simp]
                  theorem sup_sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  (ab) \ symmDiff a b = ab
                  theorem disjoint_symmDiff_inf {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  Disjoint (symmDiff a b) (ab)
                  theorem inf_symmDiff_distrib_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  asymmDiff b c = symmDiff (ab) (ac)
                  theorem inf_symmDiff_distrib_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  symmDiff a bc = symmDiff (ac) (bc)
                  theorem sdiff_symmDiff {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  c \ symmDiff a b = cabc \ ac \ b
                  theorem sdiff_symmDiff' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  c \ symmDiff a b = cabc \ (ab)
                  @[simp]
                  theorem symmDiff_sdiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff a b \ a = b \ a
                  @[simp]
                  theorem symmDiff_sdiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff a b \ b = a \ b
                  @[simp]
                  theorem sdiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  a \ symmDiff a b = ab
                  @[simp]
                  theorem sdiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  b \ symmDiff a b = ab
                  theorem symmDiff_eq_sup {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff a b = ab Disjoint a b
                  @[simp]
                  theorem le_symmDiff_iff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem le_symmDiff_iff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  theorem symmDiff_symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  symmDiff (symmDiff a b) c = a \ (bc)b \ (ac)c \ (ab)abc
                  theorem symmDiff_symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  symmDiff a (symmDiff b c) = a \ (bc)b \ (ac)c \ (ab)abc
                  theorem symmDiff_assoc {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  instance symmDiff_isAssociative {α : Type u_2} [GeneralizedBooleanAlgebra α] :
                  Std.Associative fun (x1 x2 : α) => symmDiff x1 x2
                  theorem symmDiff_left_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  theorem symmDiff_right_comm {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b c : α) :
                  @[simp]
                  theorem symmDiff_symmDiff_cancel_left {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff a (symmDiff a b) = b
                  @[simp]
                  theorem symmDiff_symmDiff_cancel_right {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff (symmDiff b a) a = b
                  @[simp]
                  theorem symmDiff_symmDiff_self' {α : Type u_2} [GeneralizedBooleanAlgebra α] (a b : α) :
                  symmDiff (symmDiff a b) a = b
                  theorem symmDiff_left_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Involutive fun (x : α) => symmDiff x a
                  theorem symmDiff_right_involutive {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Involutive fun (x : α) => symmDiff a x
                  theorem symmDiff_left_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Injective fun (x : α) => symmDiff x a
                  theorem symmDiff_right_injective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Injective fun (x : α) => symmDiff a x
                  theorem symmDiff_left_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Surjective fun (x : α) => symmDiff x a
                  theorem symmDiff_right_surjective {α : Type u_2} [GeneralizedBooleanAlgebra α] (a : α) :
                  Function.Surjective fun (x : α) => symmDiff a x
                  @[simp]
                  theorem symmDiff_left_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} :
                  symmDiff a b = symmDiff c b a = c
                  @[simp]
                  theorem symmDiff_right_inj {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} :
                  symmDiff a b = symmDiff a c b = c
                  @[simp]
                  theorem symmDiff_eq_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} :
                  symmDiff a b = a b =
                  @[simp]
                  theorem symmDiff_eq_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b : α} :
                  symmDiff a b = b a =
                  theorem Disjoint.symmDiff_left {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
                  theorem Disjoint.symmDiff_right {α : Type u_2} [GeneralizedBooleanAlgebra α] {a b c : α} (ha : Disjoint a b) (hb : Disjoint a c) :
                  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

                  @[simp]
                  theorem inf_himp_bihimp {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b ab = ab
                  theorem codisjoint_bihimp_sup {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  Codisjoint (bihimp a b) (ab)
                  @[simp]
                  theorem himp_bihimp_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  a bihimp a b = a b
                  @[simp]
                  theorem himp_bihimp_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  b bihimp a b = b a
                  @[simp]
                  theorem bihimp_himp_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b a = ab
                  @[simp]
                  theorem bihimp_himp_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b b = ab
                  @[simp]
                  theorem bihimp_eq_inf {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b = ab Codisjoint a b
                  @[simp]
                  theorem bihimp_le_iff_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem bihimp_le_iff_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  theorem bihimp_assoc {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
                  bihimp (bihimp a b) c = bihimp a (bihimp b c)
                  instance bihimp_isAssociative {α : Type u_2} [BooleanAlgebra α] :
                  Std.Associative fun (x1 x2 : α) => bihimp x1 x2
                  theorem bihimp_left_comm {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
                  bihimp a (bihimp b c) = bihimp b (bihimp a c)
                  theorem bihimp_right_comm {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
                  bihimp (bihimp a b) c = bihimp (bihimp a c) b
                  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)
                  @[simp]
                  theorem bihimp_bihimp_cancel_left {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a (bihimp a b) = b
                  @[simp]
                  theorem bihimp_bihimp_cancel_right {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp (bihimp b a) a = b
                  @[simp]
                  theorem bihimp_bihimp_self {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp (bihimp a b) a = b
                  theorem bihimp_left_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Involutive fun (x : α) => bihimp x a
                  theorem bihimp_right_involutive {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Involutive fun (x : α) => bihimp a x
                  theorem bihimp_left_injective {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Injective fun (x : α) => bihimp x a
                  theorem bihimp_right_injective {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Injective fun (x : α) => bihimp a x
                  theorem bihimp_left_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Surjective fun (x : α) => bihimp x a
                  theorem bihimp_right_surjective {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  Function.Surjective fun (x : α) => bihimp a x
                  @[simp]
                  theorem bihimp_left_inj {α : Type u_2} [BooleanAlgebra α] {a b c : α} :
                  bihimp a b = bihimp c b a = c
                  @[simp]
                  theorem bihimp_right_inj {α : Type u_2} [BooleanAlgebra α] {a b c : α} :
                  bihimp a b = bihimp a c b = c
                  @[simp]
                  theorem bihimp_eq_left {α : Type u_2} [BooleanAlgebra α] {a b : α} :
                  bihimp a b = a b =
                  @[simp]
                  theorem bihimp_eq_right {α : Type u_2} [BooleanAlgebra α] {a b : α} :
                  bihimp a b = b a =
                  theorem Codisjoint.bihimp_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
                  theorem Codisjoint.bihimp_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (ha : Codisjoint a b) (hb : Codisjoint a c) :
                  theorem symmDiff_eq {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  symmDiff a b = abba
                  theorem bihimp_eq {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b = (ab)(ba)
                  theorem symmDiff_eq' {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  symmDiff a b = (ab)(ab)
                  theorem bihimp_eq' {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  bihimp a b = abab
                  theorem symmDiff_top {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  theorem top_symmDiff {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  @[simp]
                  theorem compl_symmDiff {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  (symmDiff a b) = bihimp a b
                  @[simp]
                  theorem compl_bihimp {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  (bihimp a b) = symmDiff a b
                  @[simp]
                  theorem compl_symmDiff_compl {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem compl_bihimp_compl {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem symmDiff_eq_top {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem bihimp_eq_bot {α : Type u_2} [BooleanAlgebra α] (a b : α) :
                  @[simp]
                  theorem compl_symmDiff_self {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  @[simp]
                  theorem symmDiff_compl_self {α : Type u_2} [BooleanAlgebra α] (a : α) :
                  theorem symmDiff_symmDiff_right' {α : Type u_2} [BooleanAlgebra α] (a b c : α) :
                  symmDiff a (symmDiff b c) = abcabcabcabc
                  theorem Disjoint.le_symmDiff_sup_symmDiff_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Disjoint a b) :
                  c symmDiff a csymmDiff b c
                  theorem Disjoint.le_symmDiff_sup_symmDiff_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Disjoint b c) :
                  a symmDiff a bsymmDiff a c
                  theorem Codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Codisjoint a b) :
                  bihimp a cbihimp b c c
                  theorem Codisjoint.bihimp_inf_bihimp_le_right {α : Type u_2} [BooleanAlgebra α] {a b c : α} (h : Codisjoint b c) :
                  bihimp a bbihimp a c a

                  Prod #

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

                  Pi #

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