Mathlib.Order.SymmDiff

symmDiff definition

[Max α] [SDiff α] (a b : α) : α

Full source

/-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/
def symmDiff [Max α] [SDiff α] (a b : α) : α :=
  a \ ba \ b ⊔ b \ a

Symmetric difference of two elements

Informal description

The symmetric difference of two elements $ a $ and $ b $ in a type $ \alpha $ equipped with a join operation $ \sqcup $ and a difference operation $ \setminus $ is defined as $ (a \setminus b) \sqcup (b \setminus a) $.

bihimp definition

[Min α] [HImp α] (a b : α) : α

Full source

/-- The Heyting bi-implication is `(b ⇨ a) ⊓ (a ⇨ b)`. This generalizes equivalence of
propositions. -/
def bihimp [Min α] [HImp α] (a b : α) : α :=
  (b ⇨ a) ⊓ (a ⇨ b)

Heyting bi-implication

Informal description

The Heyting bi-implication of two elements $ a $ and $ b $ in a Heyting algebra is defined as the infimum of the Heyting implications $ (b \Rightarrow a) $ and $ (a \Rightarrow b) $. This generalizes the notion of logical equivalence for propositions.

symmDiff.term_∆_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for symmDiff -/
scoped[symmDiff] infixl:100 " ∆ " => symmDiff

Symmetric difference notation `∆`

Informal description

The notation `a ∆ b` represents the symmetric difference operation between elements `a` and `b` in a type `α` that has a supremum operation `⊔` and a set difference operation `\`. The symmetric difference is defined as `(a \ b) ⊔ (b \ a)`, which captures elements that are in exactly one of the two sets (or elements that satisfy exactly one of two properties in a more general context).

symmDiff.term_⇔_ definition

: Lean.TrailingParserDescr✝

Full source

/-- Notation for bihimp -/
scoped[symmDiff] infixl:100 " ⇔ " => bihimp

Bi-implication notation

Informal description

The notation `a ⇔ b` represents the bi-implication operator, defined as `(b ⇨ a) ⊓ (a ⇨ b)` in a (co-)Heyting algebra.

symmDiff_def theorem

[Max α] [SDiff α] (a b : α) : a ∆ b = a \ b ⊔ b \ a

Full source

theorem symmDiff_def [Max α] [SDiff α] (a b : α) : a ∆ b = a \ ba \ b ⊔ b \ a :=
  rfl

Definition of Symmetric Difference via Join and Difference

Informal description

For any two elements $a$ and $b$ in a type $\alpha$ equipped with a join operation $\sqcup$ and a difference operation $\setminus$, the symmetric difference $a \triangle b$ is equal to $(a \setminus b) \sqcup (b \setminus a)$.

bihimp_def theorem

[Min α] [HImp α] (a b : α) : a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)

Full source

theorem bihimp_def [Min α] [HImp α] (a b : α) : a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b) :=
  rfl

Definition of Bi-implication in Heyting Algebras: $a \Leftrightarrow b = (b \Rightarrow a) \sqcap (a \Rightarrow b)$

Informal description

For any elements $a$ and $b$ in a Heyting algebra with a minimum operation $\sqcap$ and Heyting implication $\Rightarrow$, the bi-implication $a \Leftrightarrow b$ is equal to $(b \Rightarrow a) \sqcap (a \Rightarrow b)$.

symmDiff_eq_Xor' theorem

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

Full source

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

Symmetric Difference Equals Exclusive-Or for Propositions: $p \triangle q = \text{Xor}(p, q)$

Informal description

For any two propositions $p$ and $q$, the symmetric difference $p \triangle q$ is equal to the exclusive-or of $p$ and $q$, i.e., $p \triangle q = \text{Xor}(p, q)$.

bihimp_iff_iff theorem

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

Full source

@[simp]
theorem bihimp_iff_iff {p q : Prop} : p ⇔ qp ⇔ q ↔ (p ↔ q) :=
  iff_iff_implies_and_implies.symm.trans Iff.comm

Bi-implication Equivalence: $p \Leftrightarrow q \leftrightarrow (p \leftrightarrow q)$

Informal description

For any propositions $p$ and $q$, the Heyting bi-implication $p \Leftrightarrow q$ holds if and only if $p$ is logically equivalent to $q$.

Bool.symmDiff_eq_xor theorem

: ∀ p q : Bool, p ∆ q = xor p q

Full source

@[simp]
theorem Bool.symmDiff_eq_xor : ∀ p q : Bool, p ∆ q = xor p q := by decide

Symmetric Difference Equals XOR on Boolean Values

Informal description

For any boolean values $p$ and $q$, the symmetric difference $p \Delta q$ is equal to the exclusive or (XOR) of $p$ and $q$, i.e., $p \Delta q = \text{xor}(p, q)$.

toDual_symmDiff theorem

: toDual (a ∆ b) = toDual a ⇔ toDual b

Full source

@[simp]
theorem toDual_symmDiff : toDual (a ∆ b) = toDualtoDual a ⇔ toDual b :=
  rfl

Dual Symmetric Difference Equals Bi-implication of Duals: $\text{toDual}(a \Delta b) = \text{toDual}(a) \Leftrightarrow \text{toDual}(b)$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra $\alpha$, the order dual of their symmetric difference $a \Delta b$ is equal to the bi-implication of their order duals, i.e., $\text{toDual}(a \Delta b) = \text{toDual}(a) \Leftrightarrow \text{toDual}(b)$.

ofDual_bihimp theorem

(a b : αᵒᵈ) : ofDual (a ⇔ b) = ofDual a ∆ ofDual b

Full source

@[simp]
theorem ofDual_bihimp (a b : αᵒᵈ) : ofDual (a ⇔ b) = ofDualofDual a ∆ ofDual b :=
  rfl

Dual Bi-implication Equals Symmetric Difference in Original Algebra

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^{\text{op}}$ of a generalized Heyting algebra, the bi-implication $a \Leftrightarrow b$ in the dual algebra corresponds to the symmetric difference $\text{ofDual}(a) \Delta \text{ofDual}(b)$ in the original algebra. That is, $\text{ofDual}(a \Leftrightarrow b) = \text{ofDual}(a) \Delta \text{ofDual}(b)$.

symmDiff_comm theorem

: a ∆ b = b ∆ a

Full source

theorem symmDiff_comm : a ∆ b = b ∆ a := by simp only [symmDiff, sup_comm]

Commutativity of Symmetric Difference: $a \Delta b = b \Delta a$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra $\alpha$, the symmetric difference operation $\Delta$ is commutative, i.e., $a \Delta b = b \Delta a$.

symmDiff_isCommutative instance

: Std.Commutative (α := α) (· ∆ ·)

Full source

instance symmDiff_isCommutative : Std.Commutative (α := α) (· ∆ ·) :=
  ⟨symmDiff_comm⟩

Commutativity of Symmetric Difference

Informal description

The symmetric difference operation $\Delta$ on a generalized co-Heyting algebra $\alpha$ is commutative.

symmDiff_self theorem

: a ∆ a = ⊥

Full source

@[simp]
theorem symmDiff_self : a ∆ a = ⊥ := by rw [symmDiff, sup_idem, sdiff_self]

Self-Symmetric Difference Equals Bottom: $a \Delta a = \bot$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the symmetric difference of $a$ with itself equals the bottom element, i.e., $a \Delta a = \bot$.

symmDiff_bot theorem

: a ∆ ⊥ = a

Full source

@[simp]
theorem symmDiff_bot : a ∆ ⊥ = a := by rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]

Symmetric Difference with Bottom Element: $a \Delta \bot = a$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the symmetric difference of $a$ with the bottom element $\bot$ equals $a$, i.e., $a \Delta \bot = a$.

bot_symmDiff theorem

: ⊥ ∆ a = a

Full source

@[simp]
theorem bot_symmDiff : ⊥⊥ ∆ a = a := by rw [symmDiff_comm, symmDiff_bot]

Symmetric Difference with Bottom Element: $\bot \Delta a = a$

Informal description

In a generalized co-Heyting algebra, the symmetric difference of the bottom element $\bot$ with any element $a$ equals $a$, i.e., $\bot \Delta a = a$.

symmDiff_eq_bot theorem

{a b : α} : a ∆ b = ⊥ ↔ a = b

Full source

@[simp]
theorem symmDiff_eq_bot {a b : α} : a ∆ ba ∆ b = ⊥ ↔ a = b := by
  simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]

Symmetric Difference Vanishes if and Only if Elements Are Equal

Informal description

For any two elements $a$ and $b$ in a generalized co-Heyting algebra $\alpha$, the symmetric difference $a \Delta b$ equals the bottom element $\bot$ if and only if $a = b$.

symmDiff_of_le theorem

{a b : α} (h : a ≤ b) : a ∆ b = b \ a

Full source

theorem symmDiff_of_le {a b : α} (h : a ≤ b) : a ∆ b = b \ a := by
  rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]

Symmetric difference of comparable elements equals their difference

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$ with $a \leq b$, the symmetric difference $a \Delta b$ equals the difference $b \setminus a$.

symmDiff_of_ge theorem

{a b : α} (h : b ≤ a) : a ∆ b = a \ b

Full source

theorem symmDiff_of_ge {a b : α} (h : b ≤ a) : a ∆ b = a \ b := by
  rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]

Symmetric difference under right inequality: $a \Delta b = a \setminus b$ when $b \leq a$

Informal description

For any two elements $a$ and $b$ in a generalized co-Heyting algebra $\alpha$, if $b \leq a$, then the symmetric difference $a \Delta b$ equals the difference $a \setminus b$.

symmDiff_le theorem

{a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ∆ b ≤ c

Full source

theorem symmDiff_le {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ∆ b ≤ c :=
  sup_le (sdiff_le_iff.2 ha) <| sdiff_le_iff.2 hb

Upper Bound for Symmetric Difference via Suprema

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, if $a \leq b \sqcup c$ and $b \leq a \sqcup c$, then the symmetric difference $a \Delta b$ satisfies $a \Delta b \leq c$.

symmDiff_le_iff theorem

{a b c : α} : a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Full source

theorem symmDiff_le_iff {a b c : α} : a ∆ ba ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c := by
  simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]

Characterization of Symmetric Difference via Supremum: $a \Delta b \leq c \leftrightarrow (a \leq b \sqcup c \land b \leq a \sqcup c)$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the symmetric difference $a \Delta b$ is less than or equal to $c$ if and only if both $a \leq b \sqcup c$ and $b \leq a \sqcup c$ hold.

symmDiff_le_sup theorem

{a b : α} : a ∆ b ≤ a ⊔ b

Full source

@[simp]
theorem symmDiff_le_sup {a b : α} : a ∆ b ≤ a ⊔ b :=
  sup_le_sup sdiff_le sdiff_le

Symmetric Difference Bounded by Supremum: $a \Delta b \leq a \sqcup b$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the symmetric difference $a \Delta b$ is less than or equal to the supremum $a \sqcup b$.

symmDiff_eq_sup_sdiff_inf theorem

: a ∆ b = (a ⊔ b) \ (a ⊓ b)

Full source

theorem symmDiff_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b) := by simp [sup_sdiff, symmDiff]

Symmetric Difference as Supremum Minus Infimum: $a \triangle b = (a \sqcup b) \setminus (a \sqcap b)$

Informal description

In a generalized co-Heyting algebra, the symmetric difference $a \triangle b$ of two elements $a$ and $b$ equals the difference between their supremum and their infimum, i.e., $$ a \triangle b = (a \sqcup b) \setminus (a \sqcap b). $$

Disjoint.symmDiff_eq_sup theorem

{a b : α} (h : Disjoint a b) : a ∆ b = a ⊔ b

Full source

theorem Disjoint.symmDiff_eq_sup {a b : α} (h : Disjoint a b) : a ∆ b = a ⊔ b := by
  rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]

Symmetric Difference of Disjoint Elements Equals Supremum: $a \triangle b = a \sqcup b$ when $a \sqcap b = \bot$

Informal description

For any two disjoint elements $a$ and $b$ in a generalized co-Heyting algebra $\alpha$ (i.e., $a \sqcap b = \bot$), their symmetric difference equals their supremum, i.e., $a \triangle b = a \sqcup b$.

symmDiff_sdiff theorem

: a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

Full source

theorem symmDiff_sdiff : a ∆ ba ∆ b \ c = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) := by
  rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

Symmetric Difference-Difference Identity: $(a \triangle b) \setminus c = (a \setminus (b \sqcup c)) \sqcup (b \setminus (a \sqcup c))$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the symmetric difference followed by difference operation satisfies: $$(a \triangle b) \setminus c = (a \setminus (b \sqcup c)) \sqcup (b \setminus (a \sqcup c))$$ where $\triangle$ denotes the symmetric difference operation defined as $a \triangle b = (a \setminus b) \sqcup (b \setminus a)$.

symmDiff_sdiff_inf theorem

: a ∆ b \ (a ⊓ b) = a ∆ b

Full source

@[simp]
theorem symmDiff_sdiff_inf : a ∆ ba ∆ b \ (a ⊓ b) = a ∆ b := by
  rw [symmDiff_sdiff]
  simp [symmDiff]

Symmetric Difference Minus Meet Equals Symmetric Difference: $(a \triangle b) \setminus (a \sqcap b) = a \triangle b$

Informal description

In a generalized co-Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the symmetric difference of $a$ and $b$ minus their meet equals the symmetric difference itself, i.e., $$(a \triangle b) \setminus (a \sqcap b) = a \triangle b$$ where $\triangle$ denotes the symmetric difference operation defined as $a \triangle b = (a \setminus b) \sqcup (b \setminus a)$.

symmDiff_sdiff_eq_sup theorem

: a ∆ (b \ a) = a ⊔ b

Full source

@[simp]
theorem symmDiff_sdiff_eq_sup : a ∆ (b \ a) = a ⊔ b := by
  rw [symmDiff, sdiff_idem]
  exact
    le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

Symmetric Difference-Difference Equals Supremum: $a \triangle (b \setminus a) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the symmetric difference of $a$ and $(b \setminus a)$ equals the supremum of $a$ and $b$, i.e., $$ a \triangle (b \setminus a) = a \sqcup b $$ where $\triangle$ denotes the symmetric difference operation defined as $(a \setminus b) \sqcup (b \setminus a)$.

sdiff_symmDiff_eq_sup theorem

: (a \ b) ∆ b = a ⊔ b

Full source

@[simp]
theorem sdiff_symmDiff_eq_sup : (a \ b) ∆ b = a ⊔ b := by
  rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

Difference-Symmetric Difference Equals Supremum: $(a \setminus b) \triangle b = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the symmetric difference of $(a \setminus b)$ and $b$ equals the supremum of $a$ and $b$, i.e., $$ (a \setminus b) \triangle b = a \sqcup b $$ where $\triangle$ denotes the symmetric difference operation defined as $(x \setminus y) \sqcup (y \setminus x)$.

symmDiff_sup_inf theorem

: a ∆ b ⊔ a ⊓ b = a ⊔ b

Full source

@[simp]
theorem symmDiff_sup_inf : a ∆ ba ∆ b ⊔ a ⊓ b = a ⊔ b := by
  refine le_antisymm (sup_le symmDiff_le_sup inf_le_sup) ?_
  rw [sup_inf_left, symmDiff]
  refine sup_le (le_inf le_sup_right ?_) (le_inf ?_ le_sup_right)
  · rw [sup_right_comm]
    exact le_sup_of_le_left le_sdiff_sup
  · rw [sup_assoc]
    exact le_sup_of_le_right le_sdiff_sup

Symmetric Difference and Meet Join to Supremum: $(a \triangle b) \sqcup (a \sqcap b) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of their symmetric difference $a \triangle b$ and their meet $a \sqcap b$ equals the join $a \sqcup b$, i.e., $$ (a \triangle b) \sqcup (a \sqcap b) = a \sqcup b. $$

inf_sup_symmDiff theorem

: a ⊓ b ⊔ a ∆ b = a ⊔ b

Full source

@[simp]
theorem inf_sup_symmDiff : a ⊓ ba ⊓ b ⊔ a ∆ b = a ⊔ b := by rw [sup_comm, symmDiff_sup_inf]

Join of Meet and Symmetric Difference Equals Supremum: $(a \sqcap b) \sqcup (a \triangle b) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the join of their meet $a \sqcap b$ and their symmetric difference $a \triangle b$ equals the join $a \sqcup b$, i.e., $$ (a \sqcap b) \sqcup (a \triangle b) = a \sqcup b. $$

symmDiff_symmDiff_inf theorem

: a ∆ b ∆ (a ⊓ b) = a ⊔ b

Full source

@[simp]
theorem symmDiff_symmDiff_inf : a ∆ ba ∆ b ∆ (a ⊓ b) = a ⊔ b := by
  rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]

Symmetric Difference Identity: $(a \triangle b) \triangle (a \sqcap b) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the symmetric difference of $a \triangle b$ and $a \sqcap b$ equals the supremum of $a$ and $b$, i.e., $$ (a \triangle b) \triangle (a \sqcap b) = a \sqcup b. $$

inf_symmDiff_symmDiff theorem

: (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

Full source

@[simp]
theorem inf_symmDiff_symmDiff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b := by
  rw [symmDiff_comm, symmDiff_symmDiff_inf]

Symmetric Difference Identity: $(a \sqcap b) \triangle (a \triangle b) = a \sqcup b$

Informal description

In a generalized co-Heyting algebra, for any elements $a$ and $b$, the symmetric difference of their meet $a \sqcap b$ and their symmetric difference $a \triangle b$ equals the supremum of $a$ and $b$, i.e., $$ (a \sqcap b) \triangle (a \triangle b) = a \sqcup b. $$

symmDiff_triangle theorem

: a ∆ c ≤ a ∆ b ⊔ b ∆ c

Full source

theorem symmDiff_triangle : a ∆ c ≤ a ∆ ba ∆ b ⊔ b ∆ c := by
  refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_
  rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]

Triangle Inequality for Symmetric Difference: $a \mathbin{∆} c \leq (a \mathbin{∆} b) \sqcup (b \mathbin{∆} c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference $a \mathbin{∆} c$ is less than or equal to the join of the symmetric differences $a \mathbin{∆} b$ and $b \mathbin{∆} c$, i.e., $$ a \mathbin{∆} c \leq (a \mathbin{∆} b) \sqcup (b \mathbin{∆} c). $$

le_symmDiff_sup_right theorem

(a b : α) : a ≤ (a ∆ b) ⊔ b

Full source

theorem le_symmDiff_sup_right (a b : α) : a ≤ (a ∆ b) ⊔ b := by
  convert symmDiff_triangle a b ⊥ <;> rw [symmDiff_bot]

Lower Bound via Symmetric Difference and Join: $a \leq (a \mathbin{∆} b) \sqcup b$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the element $a$ is less than or equal to the join of the symmetric difference $a \mathbin{∆} b$ and $b$, i.e., $$ a \leq (a \mathbin{∆} b) \sqcup b. $$

le_symmDiff_sup_left theorem

(a b : α) : b ≤ (a ∆ b) ⊔ a

Full source

theorem le_symmDiff_sup_left (a b : α) : b ≤ (a ∆ b) ⊔ a :=
  symmDiff_comm a b ▸ le_symmDiff_sup_right ..

Lower Bound via Symmetric Difference and Join: $b \leq (a \mathbin{∆} b) \sqcup a$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the element $b$ is less than or equal to the join of the symmetric difference $a \mathbin{∆} b$ and $a$, i.e., $$ b \leq (a \mathbin{∆} b) \sqcup a. $$

toDual_bihimp theorem

: toDual (a ⇔ b) = toDual a ∆ toDual b

Full source

@[simp]
theorem toDual_bihimp : toDual (a ⇔ b) = toDualtoDual a ∆ toDual b :=
  rfl

Order Dual of Bi-Implication Equals Symmetric Difference of Order Duals

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the order dual of their bi-implication $a \Leftrightarrow b$ is equal to the symmetric difference of their order duals $\text{toDual}(a) \Delta \text{toDual}(b)$.

ofDual_symmDiff theorem

(a b : αᵒᵈ) : ofDual (a ∆ b) = ofDual a ⇔ ofDual b

Full source

@[simp]
theorem ofDual_symmDiff (a b : αᵒᵈ) : ofDual (a ∆ b) = ofDualofDual a ⇔ ofDual b :=
  rfl

Symmetric Difference in Order Dual Equals Bi-Implication in Original Algebra

Informal description

For any elements $a$ and $b$ in the order dual $\alpha^\text{op}$ of a generalized Heyting algebra $\alpha$, the symmetric difference of $a$ and $b$ under the order-reversing isomorphism $\text{ofDual} : \alpha^\text{op} \to \alpha$ equals the bi-implication of $\text{ofDual}\,a$ and $\text{ofDual}\,b$ in $\alpha$. In symbols: \[ \text{ofDual}(a \mathbin{∆} b) = (\text{ofDual}\,a) \Leftrightarrow (\text{ofDual}\,b). \]

bihimp_comm theorem

: a ⇔ b = b ⇔ a

Full source

theorem bihimp_comm : a ⇔ b = b ⇔ a := by simp only [(· ⇔ ·), inf_comm]

Commutativity of Bi-Implication in Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the bi-implication operation is commutative, i.e., $a \Leftrightarrow b = b \Leftrightarrow a$.

bihimp_isCommutative instance

: Std.Commutative (α := α) (· ⇔ ·)

Full source

instance bihimp_isCommutative : Std.Commutative (α := α) (· ⇔ ·) :=
  ⟨bihimp_comm⟩

Commutativity of Bi-Implication in Heyting Algebras

Informal description

The bi-implication operation $\Leftrightarrow$ in a generalized Heyting algebra is commutative.

bihimp_self theorem

: a ⇔ a = ⊤

Full source

@[simp]
theorem bihimp_self : a ⇔ a = ⊤ := by rw [bihimp, inf_idem, himp_self]

Bi-implication Reflexivity: $a \Leftrightarrow a = \top$

Informal description

For any element $a$ in a generalized Heyting algebra, the bi-implication of $a$ with itself is equal to the top element $\top$, i.e., $a \Leftrightarrow a = \top$.

bihimp_top theorem

: a ⇔ ⊤ = a

Full source

@[simp]
theorem bihimp_top : a ⇔ ⊤ = a := by rw [bihimp, himp_top, top_himp, inf_top_eq]

Bi-implication with Top Element: $a \Leftrightarrow \top = a$

Informal description

In a generalized Heyting algebra, for any element $a$, the bi-implication of $a$ with the top element $\top$ equals $a$, i.e., $a \Leftrightarrow \top = a$.

top_bihimp theorem

: ⊤ ⇔ a = a

Full source

@[simp]
theorem top_bihimp : ⊤⊤ ⇔ a = a := by rw [bihimp_comm, bihimp_top]

Bi-implication with Top Element: $\top \Leftrightarrow a = a$

Informal description

In a generalized Heyting algebra, for any element $a$, the bi-implication of the top element $\top$ with $a$ equals $a$, i.e., $\top \Leftrightarrow a = a$.

bihimp_eq_top theorem

{a b : α} : a ⇔ b = ⊤ ↔ a = b

Full source

@[simp]
theorem bihimp_eq_top {a b : α} : a ⇔ ba ⇔ b = ⊤ ↔ a = b :=
  @symmDiff_eq_bot αᵒᵈ _ _ _

Bi-implication Equals Top if and Only if Elements Are Equal

Informal description

For any two elements $a$ and $b$ in a generalized Heyting algebra $\alpha$, the bi-implication $a \Leftrightarrow b$ equals the top element $\top$ if and only if $a = b$.

bihimp_of_le theorem

{a b : α} (h : a ≤ b) : a ⇔ b = b ⇨ a

Full source

theorem bihimp_of_le {a b : α} (h : a ≤ b) : a ⇔ b = b ⇨ a := by
  rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]

Bi-implication under inequality: $a \Leftrightarrow b = b \Rightarrow a$ when $a \leq b$

Informal description

In a generalized Heyting algebra, if $a \leq b$, then the bi-implication $a \Leftrightarrow b$ is equal to the Heyting implication $b \Rightarrow a$.

bihimp_of_ge theorem

{a b : α} (h : b ≤ a) : a ⇔ b = a ⇨ b

Full source

theorem bihimp_of_ge {a b : α} (h : b ≤ a) : a ⇔ b = a ⇨ b := by
  rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]

Bi-implication under Greater or Equal Condition: $a \Leftrightarrow b = a \Rightarrow b$ when $b \leq a$

Informal description

Let $\alpha$ be a generalized Heyting algebra. For any elements $a, b \in \alpha$ such that $b \leq a$, the bi-implication $a \Leftrightarrow b$ is equal to the Heyting implication $a \Rightarrow b$.

le_bihimp theorem

{a b c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) : a ≤ b ⇔ c

Full source

theorem le_bihimp {a b c : α} (hb : a ⊓ b ≤ c) (hc : a ⊓ c ≤ b) : a ≤ b ⇔ c :=
  le_inf (le_himp_iff.2 hc) <| le_himp_iff.2 hb

Lower Bound of Bi-implication in Generalized Heyting Algebras

Informal description

Let $\alpha$ be a generalized Heyting algebra. For any elements $a, b, c \in \alpha$, if $a \sqcap b \leq c$ and $a \sqcap c \leq b$, then $a \leq (b \Leftrightarrow c)$, where $(b \Leftrightarrow c) = (b \Rightarrow c) \sqcap (c \Rightarrow b)$ is the bi-implication of $b$ and $c$.

le_bihimp_iff theorem

{a b c : α} : a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b

Full source

theorem le_bihimp_iff {a b c : α} : a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b := by
  simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]

Characterization of Bi-implication in Generalized Heyting Algebras

Informal description

Let $\alpha$ be a generalized Heyting algebra. For any elements $a, b, c \in \alpha$, the inequality $a \leq (b \Leftrightarrow c)$ holds if and only if both $a \sqcap b \leq c$ and $a \sqcap c \leq b$ hold, where $(b \Leftrightarrow c) = (b \Rightarrow c) \sqcap (c \Rightarrow b)$ is the bi-implication of $b$ and $c$.

inf_le_bihimp theorem

{a b : α} : a ⊓ b ≤ a ⇔ b

Full source

@[simp]
theorem inf_le_bihimp {a b : α} : a ⊓ b ≤ a ⇔ b :=
  inf_le_inf le_himp le_himp

Infimum is Below Bi-implication in Generalized Heyting Algebras

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the infimum $a \sqcap b$ is less than or equal to their bi-implication $a \Leftrightarrow b$, where $a \Leftrightarrow b := (a \Rightarrow b) \sqcap (b \Rightarrow a)$.

bihimp_eq_inf_himp_inf theorem

: a ⇔ b = a ⊔ b ⇨ a ⊓ b

Full source

theorem bihimp_eq_inf_himp_inf : a ⇔ b = a ⊔ ba ⊔ b ⇨ a ⊓ b := by simp [himp_inf_distrib, bihimp]

Bi-implication as Implication from Join to Meet in Heyting Algebras

Informal description

In a generalized Heyting algebra, the bi-implication of two elements $a$ and $b$ is equal to the Heyting implication from their join to their meet, i.e., $$ a \Leftrightarrow b = (a \sqcup b) \Rightarrow (a \sqcap b). $$

Codisjoint.bihimp_eq_inf theorem

{a b : α} (h : Codisjoint a b) : a ⇔ b = a ⊓ b

Full source

theorem Codisjoint.bihimp_eq_inf {a b : α} (h : Codisjoint a b) : a ⇔ b = a ⊓ b := by
  rw [bihimp, h.himp_eq_left, h.himp_eq_right]

Bi-implication Equals Infimum for Codisjoint Elements

Informal description

In a generalized Heyting algebra, if two elements $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then their bi-implication $a \Leftrightarrow b$ is equal to their infimum $a \sqcap b$.

himp_bihimp theorem

: a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)

Full source

theorem himp_bihimp : a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) := by
  rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]

Heyting Implication of Bi-implication: $a \Rightarrow (b \Leftrightarrow c) = (a \sqcap c \Rightarrow b) \sqcap (a \sqcap b \Rightarrow c)$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b, c \in \alpha$, the Heyting implication satisfies: \[ a \Rightarrow (b \Leftrightarrow c) = (a \sqcap c \Rightarrow b) \sqcap (a \sqcap b \Rightarrow c) \] where $\Leftrightarrow$ denotes the bi-implication operation.

sup_himp_bihimp theorem

: a ⊔ b ⇨ a ⇔ b = a ⇔ b

Full source

@[simp]
theorem sup_himp_bihimp : a ⊔ ba ⊔ b ⇨ a ⇔ b = a ⇔ b := by
  rw [himp_bihimp]
  simp [bihimp]

Heyting Implication of Bi-implication under Supremum: $(a \sqcup b) \Rightarrow (a \Leftrightarrow b) = a \Leftrightarrow b$

Informal description

In a generalized Heyting algebra $\alpha$, for any elements $a, b \in \alpha$, the Heyting implication satisfies: \[ (a \sqcup b) \Rightarrow (a \Leftrightarrow b) = a \Leftrightarrow b \] where $\Leftrightarrow$ denotes the bi-implication operation.

bihimp_himp_eq_inf theorem

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

Full source

@[simp]
theorem bihimp_himp_eq_inf : a ⇔ (a ⇨ b) = a ⊓ b :=
  @symmDiff_sdiff_eq_sup αᵒᵈ _ _ _

Bi-implication of Heyting Implication Equals Meet: $a \Leftrightarrow (a \Rightarrow b) = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the bi-implication of $a$ and $(a \Rightarrow b)$ equals the meet of $a$ and $b$, i.e., $$ a \Leftrightarrow (a \Rightarrow b) = a \sqcap b $$ where $\Leftrightarrow$ denotes the bi-implication operation and $\Rightarrow$ denotes the Heyting implication.

himp_bihimp_eq_inf theorem

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

Full source

@[simp]
theorem himp_bihimp_eq_inf : (b ⇨ a) ⇔ b = a ⊓ b :=
  @sdiff_symmDiff_eq_sup αᵒᵈ _ _ _

Heyting Implication Bi-implication Meet Identity: $(b \Rightarrow a) \Leftrightarrow b = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the bi-implication of $(b \Rightarrow a)$ and $b$ equals the meet of $a$ and $b$, i.e., $$ (b \Rightarrow a) \Leftrightarrow b = a \sqcap b $$ where $\Rightarrow$ denotes the Heyting implication and $\Leftrightarrow$ denotes the bi-implication operation.

bihimp_inf_sup theorem

: a ⇔ b ⊓ (a ⊔ b) = a ⊓ b

Full source

@[simp]
theorem bihimp_inf_sup : a ⇔ ba ⇔ b ⊓ (a ⊔ b) = a ⊓ b :=
  @symmDiff_sup_inf αᵒᵈ _ _ _

Bi-implication Meet Join Equals Meet: $(a \Leftrightarrow b) \sqcap (a \sqcup b) = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the meet of their bi-implication $a \Leftrightarrow b$ and their join $a \sqcup b$ equals the meet of $a$ and $b$, i.e., $$ (a \Leftrightarrow b) \sqcap (a \sqcup b) = a \sqcap b. $$

sup_inf_bihimp theorem

: (a ⊔ b) ⊓ a ⇔ b = a ⊓ b

Full source

@[simp]
theorem sup_inf_bihimp : (a ⊔ b) ⊓ a ⇔ b = a ⊓ b :=
  @inf_sup_symmDiff αᵒᵈ _ _ _

Meet of Join and Bi-implication Equals Meet: $(a \sqcup b) \sqcap (a \Leftrightarrow b) = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the meet of their join $a \sqcup b$ and their bi-implication $a \Leftrightarrow b$ equals the meet of $a$ and $b$, i.e., $$ (a \sqcup b) \sqcap (a \Leftrightarrow b) = a \sqcap b. $$

bihimp_bihimp_sup theorem

: a ⇔ b ⇔ (a ⊔ b) = a ⊓ b

Full source

@[simp]
theorem bihimp_bihimp_sup : a ⇔ ba ⇔ b ⇔ (a ⊔ b) = a ⊓ b :=
  @symmDiff_symmDiff_inf αᵒᵈ _ _ _

Bi-implication Identity: $(a \Leftrightarrow b) \Leftrightarrow (a \sqcup b) = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the bi-implication of $a \Leftrightarrow b$ and $a \sqcup b$ equals the meet of $a$ and $b$, i.e., $$ (a \Leftrightarrow b) \Leftrightarrow (a \sqcup b) = a \sqcap b. $$

sup_bihimp_bihimp theorem

: (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b

Full source

@[simp]
theorem sup_bihimp_bihimp : (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b :=
  @inf_symmDiff_symmDiff αᵒᵈ _ _ _

Bi-implication Identity: $(a \sqcup b) \Leftrightarrow (a \Leftrightarrow b) = a \sqcap b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the bi-implication of their join $a \sqcup b$ and their bi-implication $a \Leftrightarrow b$ equals the meet of $a$ and $b$, i.e., $$ (a \sqcup b) \Leftrightarrow (a \Leftrightarrow b) = a \sqcap b. $$

bihimp_triangle theorem

: a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c

Full source

theorem bihimp_triangle : a ⇔ ba ⇔ b ⊓ b ⇔ c ≤ a ⇔ c :=
  @symmDiff_triangle αᵒᵈ _ _ _ _

Triangle Inequality for Bi-implication: $(a \Leftrightarrow b) \sqcap (b \Leftrightarrow c) \leq (a \Leftrightarrow c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the meet of the bi-implications $(a \Leftrightarrow b)$ and $(b \Leftrightarrow c)$ is less than or equal to the bi-implication $(a \Leftrightarrow c)$. In other words: $$ (a \Leftrightarrow b) \sqcap (b \Leftrightarrow c) \leq (a \Leftrightarrow c). $$

symmDiff_top' theorem

: a ∆ ⊤ = ￢a

Full source

@[simp]
theorem symmDiff_top' : a ∆ ⊤ = ￢a := by simp [symmDiff]

Symmetric Difference with Top is Negation: $a \mathbin{∆} \top = \neg a$

Informal description

In a co-Heyting algebra $\alpha$, the symmetric difference between any element $a \in \alpha$ and the top element $\top$ equals the negation of $a$, i.e., $a \mathbin{∆} \top = \neg a$.

top_symmDiff' theorem

: ⊤ ∆ a = ￢a

Full source

@[simp]
theorem top_symmDiff' : ⊤⊤ ∆ a = ￢a := by simp [symmDiff]

Symmetric Difference with Top Equals Negation: $\top \mathbin{∆} a = \neg a$

Informal description

In a co-Heyting algebra $\alpha$, the symmetric difference between the top element $\top$ and any element $a \in \alpha$ equals the negation of $a$, i.e., $\top \mathbin{∆} a = \neg a$.

hnot_symmDiff_self theorem

: (￢a) ∆ a = ⊤

Full source

@[simp]
theorem hnot_symmDiff_self : (￢a) ∆ a = ⊤ := by
  rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
  exact Codisjoint.top_le codisjoint_hnot_left

Symmetric Difference of Negation and Element is Top: $\neg a \mathbin{∆} a = \top$

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the symmetric difference between the negation $\neg a$ and $a$ equals the top element $\top$, i.e., $\neg a \mathbin{∆} a = \top$.

symmDiff_hnot_self theorem

: a ∆ (￢a) = ⊤

Full source

@[simp]
theorem symmDiff_hnot_self : a ∆ (￢a) = ⊤ := by rw [symmDiff_comm, hnot_symmDiff_self]

Symmetric Difference with Negation Yields Top: $a \mathbin{∆} \neg a = \top$

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the symmetric difference between $a$ and its negation $\neg a$ equals the top element $\top$, i.e., $a \mathbin{∆} \neg a = \top$.

IsCompl.symmDiff_eq_top theorem

{a b : α} (h : IsCompl a b) : a ∆ b = ⊤

Full source

theorem IsCompl.symmDiff_eq_top {a b : α} (h : IsCompl a b) : a ∆ b = ⊤ := by
  rw [h.eq_hnot, hnot_symmDiff_self]

Symmetric Difference of Complements is Top: $a \mathbin{∆} b = \top$ when $a$ and $b$ are complements

Informal description

In a co-Heyting algebra $\alpha$, if two elements $a$ and $b$ are complements (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$), then their symmetric difference equals the top element, i.e., $a \mathbin{∆} b = \top$.

bihimp_bot theorem

: a ⇔ ⊥ = aᶜ

Full source

@[simp]
theorem bihimp_bot : a ⇔ ⊥ = aᶜ := by simp [bihimp]

Bi-implication with Bottom Yields Pseudo-complement: $a \Leftrightarrow \bot = \neg a$

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the bi-implication of $a$ with the bottom element $\bot$ equals the pseudo-complement of $a$, i.e., $a \Leftrightarrow \bot = \neg a$.

bot_bihimp theorem

: ⊥ ⇔ a = aᶜ

Full source

@[simp]
theorem bot_bihimp : ⊥⊥ ⇔ a = aᶜ := by simp [bihimp]

Bi-implication with Bottom Yields Pseudo-complement: $\bot \Leftrightarrow a = \neg a$

Informal description

In a Heyting algebra $\alpha$, the bi-implication of the bottom element $\bot$ and any element $a$ is equal to the pseudo-complement of $a$, i.e., $\bot \Leftrightarrow a = \neg a$.

compl_bihimp_self theorem

: aᶜ ⇔ a = ⊥

Full source

@[simp]
theorem compl_bihimp_self : aᶜaᶜ ⇔ a = ⊥ :=
  @hnot_symmDiff_self αᵒᵈ _ _

Bi-implication of Pseudo-complement and Element is Bottom: $\neg a \Leftrightarrow a = \bot$

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the bi-implication of the pseudo-complement $\neg a$ and $a$ equals the bottom element $\bot$, i.e., $\neg a \Leftrightarrow a = \bot$.

bihimp_hnot_self theorem

: a ⇔ aᶜ = ⊥

Full source

@[simp]
theorem bihimp_hnot_self : a ⇔ aᶜ = ⊥ :=
  @symmDiff_hnot_self αᵒᵈ _ _

Bi-implication of Element and its Negation is Bottom: $a \Leftrightarrow \neg a = \bot$

Informal description

In a Heyting algebra $\alpha$, for any element $a \in \alpha$, the bi-implication of $a$ and its pseudo-complement $\neg a$ equals the bottom element $\bot$, i.e., $a \Leftrightarrow \neg a = \bot$.

IsCompl.bihimp_eq_bot theorem

{a b : α} (h : IsCompl a b) : a ⇔ b = ⊥

Full source

theorem IsCompl.bihimp_eq_bot {a b : α} (h : IsCompl a b) : a ⇔ b = ⊥ := by
  rw [h.eq_compl, compl_bihimp_self]

Bi-implication of Complementary Elements is Bottom: $a \Leftrightarrow b = \bot$

Informal description

Let $\alpha$ be a Heyting algebra, and let $a, b \in \alpha$ be complementary elements (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$). Then the bi-implication of $a$ and $b$ equals the bottom element, i.e., $a \Leftrightarrow b = \bot$.

sup_sdiff_symmDiff theorem

: (a ⊔ b) \ a ∆ b = a ⊓ b

Full source

@[simp]
theorem sup_sdiff_symmDiff : (a ⊔ b) \ a ∆ b = a ⊓ b :=
  sdiff_eq_symm inf_le_sup (by rw [symmDiff_eq_sup_sdiff_inf])

Supremum Minus Symmetric Difference Equals Infimum: $(a \sqcup b) \setminus (a \triangle b) = a \sqcap b$

Informal description

In a generalized co-Heyting algebra, for any two elements $a$ and $b$, the difference between their supremum and their symmetric difference equals their infimum, i.e., $$ (a \sqcup b) \setminus (a \triangle b) = a \sqcap b. $$

disjoint_symmDiff_inf theorem

: Disjoint (a ∆ b) (a ⊓ b)

Full source

theorem disjoint_symmDiff_inf : Disjoint (a ∆ b) (a ⊓ b) := by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact disjoint_sdiff_self_left

Disjointness of Symmetric Difference and Infimum: $(a \triangle b) \sqcap (a \sqcap b) = \bot$

Informal description

For any two elements $a$ and $b$ in a generalized Boolean algebra, the symmetric difference $a \triangle b$ is disjoint from their infimum $a \sqcap b$, i.e., $(a \triangle b) \sqcap (a \sqcap b) = \bot$.

inf_symmDiff_distrib_left theorem

: a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)

Full source

theorem inf_symmDiff_distrib_left : a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c) := by
  rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left,
    symmDiff_eq_sup_sdiff_inf]

Left Distributivity of Meet over Symmetric Difference: $a \sqcap (b \Delta c) = (a \sqcap b) \Delta (a \sqcap c)$

Informal description

In a lattice $\alpha$ with a symmetric difference operation $\Delta$, for any elements $a, b, c \in \alpha$, the meet operation distributes over the symmetric difference on the left: $$ a \sqcap (b \Delta c) = (a \sqcap b) \Delta (a \sqcap c). $$

inf_symmDiff_distrib_right theorem

: a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

Full source

theorem inf_symmDiff_distrib_right : a ∆ ba ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c) := by
  simp_rw [inf_comm _ c, inf_symmDiff_distrib_left]

Right Distributivity of Meet over Symmetric Difference: $(a \Delta b) \sqcap c = (a \sqcap c) \Delta (b \sqcap c)$

Informal description

In a lattice $\alpha$ with a symmetric difference operation $\Delta$, for any elements $a, b, c \in \alpha$, the meet operation distributes over the symmetric difference on the right: $$ (a \Delta b) \sqcap c = (a \sqcap c) \Delta (b \sqcap c). $$

sdiff_symmDiff theorem

: c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b

Full source

theorem sdiff_symmDiff : c \ a ∆ b = c ⊓ ac ⊓ a ⊓ bc ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b := by
  simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']

Difference of Symmetric Difference Equals Meet of Differences

Informal description

For elements $a$, $b$, and $c$ in a lattice with a difference operation $\setminus$ and symmetric difference operation $\Delta$, the following equality holds: \[ c \setminus (a \Delta b) = (c \sqcap a \sqcap b) \sqcup (c \setminus a \sqcap c \setminus b). \]

sdiff_symmDiff' theorem

: c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

Full source

theorem sdiff_symmDiff' : c \ a ∆ b = c ⊓ ac ⊓ a ⊓ bc ⊓ a ⊓ b ⊔ c \ (a ⊔ b) := by
  rw [sdiff_symmDiff, sdiff_sup]

Difference of Symmetric Difference Equals Meet and Difference of Join

Informal description

For elements $a$, $b$, and $c$ in a lattice with a difference operation $\setminus$ and symmetric difference operation $\Delta$, the following equality holds: \[ c \setminus (a \Delta b) = (c \sqcap a \sqcap b) \sqcup (c \setminus (a \sqcup b)). \]

symmDiff_sdiff_left theorem

: a ∆ b \ a = b \ a

Full source

@[simp]
theorem symmDiff_sdiff_left : a ∆ ba ∆ b \ a = b \ a := by
  rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

Left Difference of Symmetric Difference: $(a \Delta b) \setminus a = b \setminus a$

Informal description

For any elements $a$ and $b$ in a lattice with a symmetric difference operation $\Delta$ and a difference operation $\setminus$, the difference of the symmetric difference $a \Delta b$ with $a$ equals the difference of $b$ with $a$, i.e., $(a \Delta b) \setminus a = b \setminus a$.

symmDiff_sdiff_right theorem

: a ∆ b \ b = a \ b

Full source

@[simp]
theorem symmDiff_sdiff_right : a ∆ ba ∆ b \ b = a \ b := by rw [symmDiff_comm, symmDiff_sdiff_left]

Right Difference of Symmetric Difference: $(a \Delta b) \setminus b = a \setminus b$

Informal description

For any elements $a$ and $b$ in a lattice with a symmetric difference operation $\Delta$ and a difference operation $\setminus$, the difference of the symmetric difference $a \Delta b$ with $b$ equals the difference of $a$ with $b$, i.e., $(a \Delta b) \setminus b = a \setminus b$.

sdiff_symmDiff_left theorem

: a \ a ∆ b = a ⊓ b

Full source

@[simp]
theorem sdiff_symmDiff_left : a \ a ∆ b = a ⊓ b := by simp [sdiff_symmDiff]

Difference with Symmetric Difference Equals Meet: $a \setminus (a \Delta b) = a \sqcap b$

Informal description

For any elements $a$ and $b$ in a lattice with a difference operation $\setminus$ and symmetric difference operation $\Delta$, the difference $a \setminus (a \Delta b)$ equals the meet $a \sqcap b$.

sdiff_symmDiff_right theorem

: b \ a ∆ b = a ⊓ b

Full source

@[simp]
theorem sdiff_symmDiff_right : b \ a ∆ b = a ⊓ b := by
  rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]

Difference with Symmetric Difference Equals Meet: $b \setminus (a \Delta b) = a \sqcap b$

Informal description

For any elements $a$ and $b$ in a lattice with a difference operation $\setminus$ and symmetric difference operation $\Delta$, the difference $b \setminus (a \Delta b)$ equals the meet $a \sqcap b$.

symmDiff_eq_sup theorem

: a ∆ b = a ⊔ b ↔ Disjoint a b

Full source

theorem symmDiff_eq_sup : a ∆ ba ∆ b = a ⊔ b ↔ Disjoint a b := by
  refine ⟨fun h => ?_, Disjoint.symmDiff_eq_sup⟩
  rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h
  exact h.of_disjoint_inf_of_le le_sup_left

Symmetric Difference Equals Supremum if and only if Elements are Disjoint: $a \triangle b = a \sqcup b \leftrightarrow a \sqcap b = \bot$

Informal description

For any elements $a$ and $b$ in a lattice with a symmetric difference operation $\triangle$ and supremum operation $\sqcup$, the symmetric difference $a \triangle b$ equals the supremum $a \sqcup b$ if and only if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

le_symmDiff_iff_left theorem

: a ≤ a ∆ b ↔ Disjoint a b

Full source

@[simp]
theorem le_symmDiff_iff_left : a ≤ a ∆ b ↔ Disjoint a b := by
  refine ⟨fun h => ?_, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
  rw [symmDiff_eq_sup_sdiff_inf] at h
  exact disjoint_iff_inf_le.mpr (le_sdiff_right.1 <| inf_le_of_left_le h).le

Element Less Than Symmetric Difference iff Disjoint: $a \leq a \triangle b \leftrightarrow a \sqcap b = \bot$

Informal description

For any elements $a$ and $b$ in a lattice with a symmetric difference operation $\triangle$, the inequality $a \leq a \triangle b$ holds if and only if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

le_symmDiff_iff_right theorem

: b ≤ a ∆ b ↔ Disjoint a b

Full source

@[simp]
theorem le_symmDiff_iff_right : b ≤ a ∆ b ↔ Disjoint a b := by
  rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]

Right Element Less Than Symmetric Difference iff Disjoint: $b \leq a \triangle b \leftrightarrow a \sqcap b = \bot$

Informal description

For any elements $a$ and $b$ in a lattice with a symmetric difference operation $\triangle$, the inequality $b \leq a \triangle b$ holds if and only if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$).

symmDiff_symmDiff_left theorem

: a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Full source

theorem symmDiff_symmDiff_left :
    a ∆ ba ∆ b ∆ c = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
  calc
    a ∆ ba ∆ b ∆ c = a ∆ ba ∆ b \ ca ∆ b \ c ⊔ c \ a ∆ b := symmDiff_def _ _
    _ = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) := by
        { rw [sdiff_symmDiff', sup_comm (c ⊓ ac ⊓ a ⊓ b), symmDiff_sdiff] }
    _ = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c := by ac_rfl

Left-Associated Symmetric Difference Expansion: $(a \triangle b) \triangle c = (a \setminus (b \sqcup c)) \sqcup (b \setminus (a \sqcup c)) \sqcup (c \setminus (a \sqcup b)) \sqcup (a \sqcap b \sqcap c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference operation satisfies: $$(a \triangle b) \triangle c = (a \setminus (b \sqcup c)) \sqcup (b \setminus (a \sqcup c)) \sqcup (c \setminus (a \sqcup b)) \sqcup (a \sqcap b \sqcap c)$$ where $\triangle$ denotes the symmetric difference operation defined as $x \triangle y = (x \setminus y) \sqcup (y \setminus x)$.

symmDiff_symmDiff_right theorem

: a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

Full source

theorem symmDiff_symmDiff_right :
    a ∆ (b ∆ c) = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c :=
  calc
    a ∆ (b ∆ c) = a \ b ∆ ca \ b ∆ c ⊔ b ∆ c \ a := symmDiff_def _ _
    _ = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ a ⊓ b ⊓ ca \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) := by
        { rw [sdiff_symmDiff', sup_comm (a ⊓ ba ⊓ b ⊓ c), symmDiff_sdiff] }
    _ = a \ (b ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b)a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c := by ac_rfl

Right-Associative Symmetric Difference Expansion in Co-Heyting Algebras

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference operation satisfies: $$a \triangle (b \triangle c) = (a \setminus (b \sqcup c)) \sqcup (b \setminus (a \sqcup c)) \sqcup (c \setminus (a \sqcup b)) \sqcup (a \sqcap b \sqcap c)$$ where $\triangle$ denotes the symmetric difference operation defined as $x \triangle y = (x \setminus y) \sqcup (y \setminus x)$.

symmDiff_assoc theorem

: a ∆ b ∆ c = a ∆ (b ∆ c)

Full source

theorem symmDiff_assoc : a ∆ ba ∆ b ∆ c = a ∆ (b ∆ c) := by
  rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]

Associativity of Symmetric Difference: $(a \triangle b) \triangle c = a \triangle (b \triangle c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference operation $\triangle$ is associative, i.e., $$(a \triangle b) \triangle c = a \triangle (b \triangle c).$$

symmDiff_isAssociative instance

: Std.Associative (α := α) (· ∆ ·)

Full source

instance symmDiff_isAssociative : Std.Associative (α := α) (· ∆ ·) :=
  ⟨symmDiff_assoc⟩

Associativity of Symmetric Difference

Informal description

The symmetric difference operation $\triangle$ on a generalized co-Heyting algebra is associative.

symmDiff_left_comm theorem

: a ∆ (b ∆ c) = b ∆ (a ∆ c)

Full source

theorem symmDiff_left_comm : a ∆ (b ∆ c) = b ∆ (a ∆ c) := by
  simp_rw [← symmDiff_assoc, symmDiff_comm]

Left-Commutativity of Symmetric Difference: $a \Delta (b \Delta c) = b \Delta (a \Delta c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra $\alpha$, the symmetric difference operation $\Delta$ satisfies the left-commutativity property: \[ a \Delta (b \Delta c) = b \Delta (a \Delta c). \]

symmDiff_right_comm theorem

: a ∆ b ∆ c = a ∆ c ∆ b

Full source

theorem symmDiff_right_comm : a ∆ ba ∆ b ∆ c = a ∆ ca ∆ c ∆ b := by simp_rw [symmDiff_assoc, symmDiff_comm]

Right-Commutativity of Symmetric Difference: $a \triangle b \triangle c = a \triangle c \triangle b$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference operation $\triangle$ satisfies the right-commutativity property: $$a \triangle b \triangle c = a \triangle c \triangle b.$$

symmDiff_symmDiff_symmDiff_comm theorem

: a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

Full source

theorem symmDiff_symmDiff_symmDiff_comm : a ∆ ba ∆ b ∆ (c ∆ d) = a ∆ ca ∆ c ∆ (b ∆ d) := by
  simp_rw [symmDiff_assoc, symmDiff_left_comm]

Commutativity of Nested Symmetric Differences: $a \triangle b \triangle (c \triangle d) = a \triangle c \triangle (b \triangle d)$

Informal description

For any elements $a$, $b$, $c$, and $d$ in a generalized co-Heyting algebra, the symmetric difference operation $\triangle$ satisfies the following commutativity property: $$a \triangle b \triangle (c \triangle d) = a \triangle c \triangle (b \triangle d).$$

symmDiff_symmDiff_cancel_left theorem

: a ∆ (a ∆ b) = b

Full source

@[simp]
theorem symmDiff_symmDiff_cancel_left : a ∆ (a ∆ b) = b := by simp [← symmDiff_assoc]

Left Cancellation Property for Symmetric Difference: $a \Delta (a \Delta b) = b$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the symmetric difference operation $\Delta$ satisfies the left cancellation property: $$a \Delta (a \Delta b) = b.$$

symmDiff_symmDiff_cancel_right theorem

: b ∆ a ∆ a = b

Full source

@[simp]
theorem symmDiff_symmDiff_cancel_right : b ∆ ab ∆ a ∆ a = b := by simp [symmDiff_assoc]

Right Cancellation Property for Symmetric Difference: $b \triangle a \triangle a = b$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the symmetric difference operation $\triangle$ satisfies the right cancellation property: $$b \triangle a \triangle a = b.$$

symmDiff_symmDiff_self' theorem

: a ∆ b ∆ a = b

Full source

@[simp]
theorem symmDiff_symmDiff_self' : a ∆ ba ∆ b ∆ a = b := by
  rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]

Involutive Property of Symmetric Difference: $a \Delta b \Delta a = b$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the symmetric difference operation $\Delta$ satisfies the involutive property: $$a \Delta b \Delta a = b.$$

symmDiff_left_involutive theorem

(a : α) : Involutive (· ∆ a)

Full source

theorem symmDiff_left_involutive (a : α) : Involutive (· ∆ a) :=
  symmDiff_symmDiff_cancel_right _

Involutive Property of Left Symmetric Difference: $(b \triangle a) \triangle a = b$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the function $f(b) = b \triangle a$ is involutive, meaning that $f(f(b)) = b$ for all $b$. In other words, applying the symmetric difference with $a$ twice returns the original element: $(b \triangle a) \triangle a = b$.

symmDiff_right_involutive theorem

(a : α) : Involutive (a ∆ ·)

Full source

theorem symmDiff_right_involutive (a : α) : Involutive (a ∆ ·) :=
  symmDiff_symmDiff_cancel_left _

Involutive Property of Right Symmetric Difference: $a \triangle (a \triangle b) = b$

Informal description

For any fixed element $a$ in a generalized co-Heyting algebra, the function $f(b) = a \triangle b$ is involutive, meaning that $f(f(b)) = b$ for all $b$. In other words, applying the symmetric difference with $a$ twice returns the original element: $a \triangle (a \triangle b) = b$.

symmDiff_left_injective theorem

(a : α) : Injective (· ∆ a)

Full source

theorem symmDiff_left_injective (a : α) : Injective (· ∆ a) :=
  Function.Involutive.injective (symmDiff_left_involutive a)

Injectivity of Left Symmetric Difference: $b_1 \triangle a = b_2 \triangle a \implies b_1 = b_2$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the function $f(b) = b \triangle a$ is injective, meaning that for any elements $b_1, b_2$, if $b_1 \triangle a = b_2 \triangle a$, then $b_1 = b_2$.

symmDiff_right_injective theorem

(a : α) : Injective (a ∆ ·)

Full source

theorem symmDiff_right_injective (a : α) : Injective (a ∆ ·) :=
  Function.Involutive.injective (symmDiff_right_involutive _)

Injectivity of Right Symmetric Difference: $a \triangle b_1 = a \triangle b_2 \implies b_1 = b_2$

Informal description

For any fixed element $a$ in a generalized co-Heyting algebra, the function $f(b) = a \triangle b$ is injective, meaning that for any elements $b_1, b_2$, if $a \triangle b_1 = a \triangle b_2$, then $b_1 = b_2$.

symmDiff_left_surjective theorem

(a : α) : Surjective (· ∆ a)

Full source

theorem symmDiff_left_surjective (a : α) : Surjective (· ∆ a) :=
  Function.Involutive.surjective (symmDiff_left_involutive _)

Surjectivity of Left Symmetric Difference: $b \triangle a$ is surjective for any $a$

Informal description

For any element $a$ in a generalized co-Heyting algebra, the function $f(b) = b \triangle a$ is surjective, meaning that for every element $c$ in the algebra, there exists an element $b$ such that $b \triangle a = c$.

symmDiff_right_surjective theorem

(a : α) : Surjective (a ∆ ·)

Full source

theorem symmDiff_right_surjective (a : α) : Surjective (a ∆ ·) :=
  Function.Involutive.surjective (symmDiff_right_involutive _)

Surjectivity of Right Symmetric Difference: $a \triangle b$ is surjective for any $a$

Informal description

For any fixed element $a$ in a generalized co-Heyting algebra, the function $f(b) = a \triangle b$ is surjective. That is, for every element $c$ in the algebra, there exists an element $b$ such that $a \triangle b = c$.

symmDiff_left_inj theorem

: a ∆ b = c ∆ b ↔ a = c

Full source

@[simp]
theorem symmDiff_left_inj : a ∆ ba ∆ b = c ∆ b ↔ a = c :=
  (symmDiff_left_injective _).eq_iff

Injectivity of Symmetric Difference in Left Argument: $a \triangle b = c \triangle b \iff a = c$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference $a \triangle b$ equals $c \triangle b$ if and only if $a = c$.

symmDiff_right_inj theorem

: a ∆ b = a ∆ c ↔ b = c

Full source

@[simp]
theorem symmDiff_right_inj : a ∆ ba ∆ b = a ∆ c ↔ b = c :=
  (symmDiff_right_injective _).eq_iff

Injectivity of Symmetric Difference in Right Argument: $a \triangle b = a \triangle c \iff b = c$

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, the symmetric difference $a \triangle b$ equals $a \triangle c$ if and only if $b = c$.

symmDiff_eq_left theorem

: a ∆ b = a ↔ b = ⊥

Full source

@[simp]
theorem symmDiff_eq_left : a ∆ ba ∆ b = a ↔ b = ⊥ :=
  calc
    a ∆ b = a ↔ a ∆ b = a ∆ ⊥ := by rw [symmDiff_bot]
    _ ↔ b = ⊥ := by rw [symmDiff_right_inj]

Symmetric Difference Equals Left Operand if and only if Right Operand is Bottom: $a \triangle b = a \iff b = \bot$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the symmetric difference $a \triangle b$ equals $a$ if and only if $b$ is the bottom element $\bot$.

symmDiff_eq_right theorem

: a ∆ b = b ↔ a = ⊥

Full source

@[simp]
theorem symmDiff_eq_right : a ∆ ba ∆ b = b ↔ a = ⊥ := by rw [symmDiff_comm, symmDiff_eq_left]

Symmetric Difference Equals Right Operand if and only if Left Operand is Bottom: $a \triangle b = b \iff a = \bot$

Informal description

For any elements $a$ and $b$ in a generalized co-Heyting algebra, the symmetric difference $a \triangle b$ equals $b$ if and only if $a$ is the bottom element $\bot$.

Disjoint.symmDiff_left theorem

(ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ∆ b) c

Full source

protected theorem Disjoint.symmDiff_left (ha : Disjoint a c) (hb : Disjoint b c) :
    Disjoint (a ∆ b) c := by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact (ha.sup_left hb).disjoint_sdiff_left

Disjointness Preservation Under Symmetric Difference

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, if $a$ and $c$ are disjoint (i.e., $a \sqcap c = \bot$) and $b$ and $c$ are disjoint (i.e., $b \sqcap c = \bot$), then the symmetric difference $a \triangle b$ and $c$ are also disjoint, i.e., $(a \triangle b) \sqcap c = \bot$.

Disjoint.symmDiff_right theorem

(ha : Disjoint a b) (hb : Disjoint a c) : Disjoint a (b ∆ c)

Full source

protected theorem Disjoint.symmDiff_right (ha : Disjoint a b) (hb : Disjoint a c) :
    Disjoint a (b ∆ c) :=
  (ha.symm.symmDiff_left hb.symm).symm

Disjointness Preservation Under Symmetric Difference (Right Variant)

Informal description

For any elements $a$, $b$, and $c$ in a generalized co-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$) and $a$ and $c$ are disjoint (i.e., $a \sqcap c = \bot$), then $a$ and the symmetric difference $b \triangle c$ are also disjoint, i.e., $a \sqcap (b \triangle c) = \bot$.

symmDiff_eq_iff_sdiff_eq theorem

(ha : a ≤ c) : a ∆ b = c ↔ c \ a = b

Full source

theorem symmDiff_eq_iff_sdiff_eq (ha : a ≤ c) : a ∆ ba ∆ b = c ↔ c \ a = b := by
  rw [← symmDiff_of_le ha]
  exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm

Characterization of symmetric difference via difference: $a \triangle b = c \leftrightarrow c \setminus a = b$ under $a \leq c$

Informal description

Let $a, b, c$ be elements in a generalized co-Heyting algebra with $a \leq c$. Then the symmetric difference $a \triangle b$ equals $c$ if and only if the difference $c \setminus a$ equals $b$.

inf_himp_bihimp theorem

: a ⇔ b ⇨ a ⊓ b = a ⊔ b

Full source

@[simp]
theorem inf_himp_bihimp : a ⇔ ba ⇔ b ⇨ a ⊓ b = a ⊔ b :=
  @sup_sdiff_symmDiff αᵒᵈ _ _ _

Bi-implication Implication to Infimum Equals Supremum: $(a \Leftrightarrow b) \Rightarrow (a \sqcap b) = a \sqcup b$

Informal description

In a Heyting algebra, the Heyting implication from the bi-implication $a \Leftrightarrow b$ to the infimum $a \sqcap b$ equals the supremum $a \sqcup b$, i.e., $$ (a \Leftrightarrow b) \Rightarrow (a \sqcap b) = a \sqcup b. $$

codisjoint_bihimp_sup theorem

: Codisjoint (a ⇔ b) (a ⊔ b)

Full source

theorem codisjoint_bihimp_sup : Codisjoint (a ⇔ b) (a ⊔ b) :=
  @disjoint_symmDiff_inf αᵒᵈ _ _ _

Codisjointness of Bi-implication and Join: $(a \Leftrightarrow b) \sqcup (a \sqcup b) = \top$

Informal description

In a Heyting algebra, the bi-implication $a \Leftrightarrow b$ and the join $a \sqcup b$ are codisjoint, i.e., $(a \Leftrightarrow b) \sqcup (a \sqcup b) = \top$.

himp_bihimp_left theorem

: a ⇨ a ⇔ b = a ⇨ b

Full source

@[simp]
theorem himp_bihimp_left : a ⇨ a ⇔ b = a ⇨ b :=
  @symmDiff_sdiff_left αᵒᵈ _ _ _

Implication of Bi-implication Equals Implication: $a \Rightarrow (a \Leftrightarrow b) = (a \Rightarrow b)$

Informal description

In a Heyting algebra, the Heyting implication of $a$ and the bi-implication $a \Leftrightarrow b$ is equal to the Heyting implication of $a$ and $b$, i.e., $a \Rightarrow (a \Leftrightarrow b) = (a \Rightarrow b)$.

himp_bihimp_right theorem

: b ⇨ a ⇔ b = b ⇨ a

Full source

@[simp]
theorem himp_bihimp_right : b ⇨ a ⇔ b = b ⇨ a :=
  @symmDiff_sdiff_right αᵒᵈ _ _ _

Implication of Bi-implication Equals Implication: $b \Rightarrow (a \Leftrightarrow b) = (b \Rightarrow a)$

Informal description

In a Heyting algebra, the Heyting implication of $b$ and the bi-implication $a \Leftrightarrow b$ is equal to the Heyting implication of $b$ and $a$, i.e., $b \Rightarrow (a \Leftrightarrow b) = (b \Rightarrow a)$.

bihimp_himp_left theorem

: a ⇔ b ⇨ a = a ⊔ b

Full source

@[simp]
theorem bihimp_himp_left : a ⇔ ba ⇔ b ⇨ a = a ⊔ b :=
  @sdiff_symmDiff_left αᵒᵈ _ _ _

Bi-implication Implication Equals Join: $(a \Leftrightarrow b) \Rightarrow a = a \sqcup b$

Informal description

In a Heyting algebra, the Heyting implication of the bi-implication $a \Leftrightarrow b$ and $a$ equals the join of $a$ and $b$, i.e., $(a \Leftrightarrow b) \Rightarrow a = a \sqcup b$.

bihimp_himp_right theorem

: a ⇔ b ⇨ b = a ⊔ b

Full source

@[simp]
theorem bihimp_himp_right : a ⇔ ba ⇔ b ⇨ b = a ⊔ b :=
  @sdiff_symmDiff_right αᵒᵈ _ _ _

Bi-implication Implication Equals Join: $(a \Leftrightarrow b) \Rightarrow b = a \sqcup b$

Informal description

In a Heyting algebra, the Heyting implication of the bi-implication $a \Leftrightarrow b$ and $b$ equals the join of $a$ and $b$, i.e., $(a \Leftrightarrow b) \Rightarrow b = a \sqcup b$.

bihimp_eq_inf theorem

: a ⇔ b = a ⊓ b ↔ Codisjoint a b

Full source

@[simp]
theorem bihimp_eq_inf : a ⇔ ba ⇔ b = a ⊓ b ↔ Codisjoint a b :=
  @symmDiff_eq_sup αᵒᵈ _ _ _

Bi-implication Equals Infimum if and only if Elements are Codisjoint: $a \Leftrightarrow b = a \sqcap b \leftrightarrow a \sqcup b = \top$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals the infimum $a \sqcap b$ if and only if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$).

bihimp_le_iff_left theorem

: a ⇔ b ≤ a ↔ Codisjoint a b

Full source

@[simp]
theorem bihimp_le_iff_left : a ⇔ ba ⇔ b ≤ a ↔ Codisjoint a b :=
  @le_symmDiff_iff_left αᵒᵈ _ _ _

Bi-implication Bound by Left Element iff Codisjoint: $a \Leftrightarrow b \leq a \leftrightarrow a \sqcup b = \top$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the bi-implication $a \Leftrightarrow b$ is less than or equal to $a$ if and only if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$).

bihimp_le_iff_right theorem

: a ⇔ b ≤ b ↔ Codisjoint a b

Full source

@[simp]
theorem bihimp_le_iff_right : a ⇔ ba ⇔ b ≤ b ↔ Codisjoint a b :=
  @le_symmDiff_iff_right αᵒᵈ _ _ _

Bi-implication Bound by Right Element iff Codisjoint: $a \Leftrightarrow b \leq b \leftrightarrow a \sqcup b = \top$

Informal description

For any elements $a$ and $b$ in a Heyting algebra, the bi-implication $a \Leftrightarrow b$ is less than or equal to $b$ if and only if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$).

bihimp_assoc theorem

: a ⇔ b ⇔ c = a ⇔ (b ⇔ c)

Full source

theorem bihimp_assoc : a ⇔ ba ⇔ b ⇔ c = a ⇔ (b ⇔ c) :=
  @symmDiff_assoc αᵒᵈ _ _ _ _

Associativity of Bi-Implication: $(a \Leftrightarrow b) \Leftrightarrow c = a \Leftrightarrow (b \Leftrightarrow c)$

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the bi-implication operation $\Leftrightarrow$ is associative, i.e., $$(a \Leftrightarrow b) \Leftrightarrow c = a \Leftrightarrow (b \Leftrightarrow c).$$

bihimp_isAssociative instance

: Std.Associative (α := α) (· ⇔ ·)

Full source

instance bihimp_isAssociative : Std.Associative (α := α) (· ⇔ ·) :=
  ⟨bihimp_assoc⟩

Associativity of Bi-Implication

Informal description

The bi-implication operation $\Leftrightarrow$ in a generalized Heyting algebra is associative.

bihimp_left_comm theorem

: a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)

Full source

theorem bihimp_left_comm : a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c) := by simp_rw [← bihimp_assoc, bihimp_comm]

Left Commutativity of Bi-Implication in Heyting Algebras

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the bi-implication operation satisfies the left commutativity property: $a \Leftrightarrow (b \Leftrightarrow c) = b \Leftrightarrow (a \Leftrightarrow c)$.

bihimp_right_comm theorem

: a ⇔ b ⇔ c = a ⇔ c ⇔ b

Full source

theorem bihimp_right_comm : a ⇔ ba ⇔ b ⇔ c = a ⇔ ca ⇔ c ⇔ b := by simp_rw [bihimp_assoc, bihimp_comm]

Right Commutativity of Bi-Implication in Heyting Algebras

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the bi-implication operation satisfies the right commutativity property: $$(a \Leftrightarrow b) \Leftrightarrow c = (a \Leftrightarrow c) \Leftrightarrow b.$$

bihimp_bihimp_bihimp_comm theorem

: a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)

Full source

theorem bihimp_bihimp_bihimp_comm : a ⇔ ba ⇔ b ⇔ (c ⇔ d) = a ⇔ ca ⇔ c ⇔ (b ⇔ d) := by
  simp_rw [bihimp_assoc, bihimp_left_comm]

Interchange Property of Bi-Implication: $a \Leftrightarrow b \Leftrightarrow (c \Leftrightarrow d) = a \Leftrightarrow c \Leftrightarrow (b \Leftrightarrow d)$

Informal description

For any elements $a$, $b$, $c$, and $d$ in a generalized Heyting algebra, the bi-implication operation satisfies the interchange property: $$a \Leftrightarrow b \Leftrightarrow (c \Leftrightarrow d) = a \Leftrightarrow c \Leftrightarrow (b \Leftrightarrow d).$$

bihimp_bihimp_cancel_left theorem

: a ⇔ (a ⇔ b) = b

Full source

@[simp]
theorem bihimp_bihimp_cancel_left : a ⇔ (a ⇔ b) = b := by simp [← bihimp_assoc]

Left Cancellation Law for Bi-implication: $a \Leftrightarrow (a \Leftrightarrow b) = b$

Informal description

In a generalized Heyting algebra, for any elements $a$ and $b$, the bi-implication of $a$ with the bi-implication of $a$ and $b$ equals $b$, i.e., $a \Leftrightarrow (a \Leftrightarrow b) = b$.

bihimp_bihimp_cancel_right theorem

: b ⇔ a ⇔ a = b

Full source

@[simp]
theorem bihimp_bihimp_cancel_right : b ⇔ ab ⇔ a ⇔ a = b := by simp [bihimp_assoc]

Right Cancellation Property of Bi-implication: $b \Leftrightarrow a \Leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the bi-implication operation satisfies $b \Leftrightarrow a \Leftrightarrow a = b$.

bihimp_bihimp_self theorem

: a ⇔ b ⇔ a = b

Full source

@[simp]
theorem bihimp_bihimp_self : a ⇔ ba ⇔ b ⇔ a = b := by rw [bihimp_comm, bihimp_bihimp_cancel_left]

Self-Cancellation Property of Bi-Implication: $a \Leftrightarrow b \Leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the bi-implication operation satisfies $a \Leftrightarrow b \Leftrightarrow a = b$.

bihimp_left_involutive theorem

(a : α) : Involutive (· ⇔ a)

Full source

theorem bihimp_left_involutive (a : α) : Involutive (· ⇔ a) :=
  bihimp_bihimp_cancel_right _

Involutivity of Left Bi-implication: $(b \Leftrightarrow a) \Leftrightarrow a = b$

Informal description

For any element $a$ in a generalized Heyting algebra, the function $f(b) = b \Leftrightarrow a$ is involutive, meaning that $f(f(b)) = b$ for all $b$ in the algebra.

bihimp_right_involutive theorem

(a : α) : Involutive (a ⇔ ·)

Full source

theorem bihimp_right_involutive (a : α) : Involutive (a ⇔ ·) :=
  bihimp_bihimp_cancel_left _

Right Bi-implication is Involutive: $(a \Leftrightarrow (a \Leftrightarrow b)) = b$

Informal description

For any element $a$ in a generalized Heyting algebra $\alpha$, the function $f(b) = a \Leftrightarrow b$ is involutive, meaning that $f(f(b)) = b$ for all $b \in \alpha$.

bihimp_left_injective theorem

(a : α) : Injective (· ⇔ a)

Full source

theorem bihimp_left_injective (a : α) : Injective (· ⇔ a) :=
  @symmDiff_left_injective αᵒᵈ _ _

Injectivity of Left Bi-implication: $b_1 \Leftrightarrow a = b_2 \Leftrightarrow a \implies b_1 = b_2$

Informal description

For any element $a$ in a generalized Heyting algebra $\alpha$, the function $f(b) = b \Leftrightarrow a$ is injective, meaning that for any elements $b_1, b_2 \in \alpha$, if $b_1 \Leftrightarrow a = b_2 \Leftrightarrow a$, then $b_1 = b_2$.

bihimp_right_injective theorem

(a : α) : Injective (a ⇔ ·)

Full source

theorem bihimp_right_injective (a : α) : Injective (a ⇔ ·) :=
  @symmDiff_right_injective αᵒᵈ _ _

Injectivity of Right Bi-implication: $a \Leftrightarrow b_1 = a \Leftrightarrow b_2 \implies b_1 = b_2$

Informal description

For any fixed element $a$ in a generalized Heyting algebra $\alpha$, the function $f(b) = a \Leftrightarrow b$ is injective. That is, for any elements $b_1, b_2 \in \alpha$, if $a \Leftrightarrow b_1 = a \Leftrightarrow b_2$, then $b_1 = b_2$.

bihimp_left_surjective theorem

(a : α) : Surjective (· ⇔ a)

Full source

theorem bihimp_left_surjective (a : α) : Surjective (· ⇔ a) :=
  @symmDiff_left_surjective αᵒᵈ _ _

Surjectivity of Left Bi-Implication in Bi-Heyting Algebras

Informal description

For any element $a$ in a bi-Heyting algebra $\alpha$, the function $f(b) = a \Leftrightarrow b$ is surjective. That is, for every element $c \in \alpha$, there exists an element $b \in \alpha$ such that $a \Leftrightarrow b = c$.

bihimp_right_surjective theorem

(a : α) : Surjective (a ⇔ ·)

Full source

theorem bihimp_right_surjective (a : α) : Surjective (a ⇔ ·) :=
  @symmDiff_right_surjective αᵒᵈ _ _

Surjectivity of Right Bi-Implication in Bi-Heyting Algebras

Informal description

For any element $a$ in a bi-Heyting algebra $\alpha$, the function $f(b) = a \Leftrightarrow b$ is surjective. That is, for every element $c \in \alpha$, there exists an element $b \in \alpha$ such that $a \Leftrightarrow b = c$.

bihimp_left_inj theorem

: a ⇔ b = c ⇔ b ↔ a = c

Full source

@[simp]
theorem bihimp_left_inj : a ⇔ ba ⇔ b = c ⇔ b ↔ a = c :=
  (bihimp_left_injective _).eq_iff

Injectivity of Left Bi-implication: $a \Leftrightarrow b = c \Leftrightarrow b \iff a = c$

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals $c \Leftrightarrow b$ if and only if $a = c$.

bihimp_right_inj theorem

: a ⇔ b = a ⇔ c ↔ b = c

Full source

@[simp]
theorem bihimp_right_inj : a ⇔ ba ⇔ b = a ⇔ c ↔ b = c :=
  (bihimp_right_injective _).eq_iff

Injectivity of Right Bi-implication: $a \Leftrightarrow b = a \Leftrightarrow c \iff b = c$

Informal description

For any elements $a$, $b$, and $c$ in a generalized Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals $a \Leftrightarrow c$ if and only if $b = c$.

bihimp_eq_left theorem

: a ⇔ b = a ↔ b = ⊤

Full source

@[simp]
theorem bihimp_eq_left : a ⇔ ba ⇔ b = a ↔ b = ⊤ :=
  @symmDiff_eq_left αᵒᵈ _ _ _

Bi-implication Equals Left Operand if and only if Right Operand is Top: $a \Leftrightarrow b = a \iff b = \top$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals $a$ if and only if $b$ is the top element $\top$.

bihimp_eq_right theorem

: a ⇔ b = b ↔ a = ⊤

Full source

@[simp]
theorem bihimp_eq_right : a ⇔ ba ⇔ b = b ↔ a = ⊤ :=
  @symmDiff_eq_right αᵒᵈ _ _ _

Bi-implication Equals Right Operand if and only if Left Operand is Top: $a \Leftrightarrow b = b \iff a = \top$

Informal description

For any elements $a$ and $b$ in a generalized Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals $b$ if and only if $a$ is the top element $\top$.

Codisjoint.bihimp_left theorem

(ha : Codisjoint a c) (hb : Codisjoint b c) : Codisjoint (a ⇔ b) c

Full source

protected theorem Codisjoint.bihimp_left (ha : Codisjoint a c) (hb : Codisjoint b c) :
    Codisjoint (a ⇔ b) c :=
  (ha.inf_left hb).mono_left inf_le_bihimp

Codisjointness Preservation Under Bi-implication

Informal description

For any elements $a$, $b$, and $c$ in a bi-Heyting algebra, if $a$ and $c$ are codisjoint (i.e., $a \sqcup c = \top$) and $b$ and $c$ are codisjoint, then the bi-implication $a \Leftrightarrow b$ and $c$ are also codisjoint.

Codisjoint.bihimp_right theorem

(ha : Codisjoint a b) (hb : Codisjoint a c) : Codisjoint a (b ⇔ c)

Full source

protected theorem Codisjoint.bihimp_right (ha : Codisjoint a b) (hb : Codisjoint a c) :
    Codisjoint a (b ⇔ c) :=
  (ha.inf_right hb).mono_right inf_le_bihimp

Codisjointness Preserved Under Bi-implication on the Right

Informal description

Let $a$, $b$, and $c$ be elements in a bi-Heyting algebra. If $a$ is codisjoint with $b$ and $a$ is codisjoint with $c$, then $a$ is codisjoint with the bi-implication $b \Leftrightarrow c$.

symmDiff_eq theorem

: a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

Full source

theorem symmDiff_eq : a ∆ b = a ⊓ bᶜa ⊓ bᶜ ⊔ b ⊓ aᶜ := by simp only [(· ∆ ·), sdiff_eq]

Symmetric Difference Formula in Co-Heyting Algebras: $a \Delta b = (a \sqcap b^c) \sqcup (b \sqcap a^c)$

Informal description

In a co-Heyting algebra, the symmetric difference $a \Delta b$ of two elements $a$ and $b$ is equal to $(a \sqcap b^c) \sqcup (b \sqcap a^c)$, where $a^c$ and $b^c$ denote the complements of $a$ and $b$ respectively.

bihimp_eq theorem

: a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)

Full source

theorem bihimp_eq : a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ) := by simp only [(· ⇔ ·), himp_eq]

Bi-implication as Meet of Complements in Bi-Heyting Algebra

Informal description

In a bi-Heyting algebra, the bi-implication operation $\Leftrightarrow$ between two elements $a$ and $b$ is given by $(a \sqcup b^c) \sqcap (b \sqcup a^c)$, where $\sqcup$ denotes the join, $\sqcap$ denotes the meet, and $(\cdot)^c$ denotes the complement.

symmDiff_eq' theorem

: a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Full source

theorem symmDiff_eq' : a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ) := by
  rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]

Symmetric Difference as Meet of Joins: $a \triangle b = (a \sqcup b) \sqcap (a^c \sqcup b^c)$

Informal description

In a co-Heyting algebra, the symmetric difference $a \triangle b$ of two elements $a$ and $b$ is equal to the meet of their join and the join of their complements, i.e., $$ a \triangle b = (a \sqcup b) \sqcap (a^c \sqcup b^c). $$

bihimp_eq' theorem

: a ⇔ b = a ⊓ b ⊔ aᶜ ⊓ bᶜ

Full source

theorem bihimp_eq' : a ⇔ b = a ⊓ ba ⊓ b ⊔ aᶜ ⊓ bᶜ :=
  @symmDiff_eq' αᵒᵈ _ _ _

Bi-implication as Join of Meet and Complements: $a \Leftrightarrow b = (a \sqcap b) \sqcup (a^c \sqcap b^c)$

Informal description

In a bi-Heyting algebra, the bi-implication $a \Leftrightarrow b$ of two elements $a$ and $b$ is equal to the join of their meet and the meet of their complements, i.e., $$ a \Leftrightarrow b = (a \sqcap b) \sqcup (a^c \sqcap b^c). $$

symmDiff_top theorem

: a ∆ ⊤ = aᶜ

Full source

theorem symmDiff_top : a ∆ ⊤ = aᶜ :=
  symmDiff_top' _

Symmetric difference with top equals complement: $a \mathbin{∆} \top = a^c$

Informal description

In a co-Heyting algebra, the symmetric difference between an element $a$ and the top element $\top$ equals the complement of $a$, i.e., $a \mathbin{∆} \top = a^c$.

top_symmDiff theorem

: ⊤ ∆ a = aᶜ

Full source

theorem top_symmDiff : ⊤⊤ ∆ a = aᶜ :=
  top_symmDiff' _

Symmetric difference with top equals complement: $\top \mathbin{∆} a = a^c$

Informal description

In a co-Heyting algebra, the symmetric difference between the top element $\top$ and any element $a$ equals the complement of $a$, i.e., $\top \mathbin{∆} a = a^c$.

compl_symmDiff theorem

: (a ∆ b)ᶜ = a ⇔ b

Full source

@[simp]
theorem compl_symmDiff : (a ∆ b)ᶜ = a ⇔ b := by
  simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]

Complement of Symmetric Difference Equals Bi-implication: $(a \mathbin{∆} b)^c = a \Leftrightarrow b$

Informal description

In a co-Heyting algebra, the complement of the symmetric difference of two elements $a$ and $b$ equals their bi-implication, i.e., $(a \mathbin{∆} b)^c = a \Leftrightarrow b$.

compl_bihimp theorem

: (a ⇔ b)ᶜ = a ∆ b

Full source

@[simp]
theorem compl_bihimp : (a ⇔ b)ᶜ = a ∆ b :=
  @compl_symmDiff αᵒᵈ _ _ _

Complement of Bi-implication Equals Symmetric Difference: $(a \Leftrightarrow b)^c = a \mathbin{∆} b$

Informal description

In a co-Heyting algebra, the complement of the bi-implication of two elements $a$ and $b$ equals their symmetric difference, i.e., $(a \Leftrightarrow b)^c = a \mathbin{∆} b$.

compl_symmDiff_compl theorem

: aᶜ ∆ bᶜ = a ∆ b

Full source

@[simp]
theorem compl_symmDiff_compl : aᶜaᶜ ∆ bᶜ = a ∆ b :=
  (sup_comm _ _).trans <| by simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

Symmetric Difference Invariance Under Complementation: $a^c \Delta b^c = a \Delta b$

Informal description

For any elements $a$ and $b$ in a co-Heyting algebra, the symmetric difference of their complements equals the symmetric difference of the original elements, i.e., $a^c \Delta b^c = a \Delta b$.

compl_bihimp_compl theorem

: aᶜ ⇔ bᶜ = a ⇔ b

Full source

@[simp]
theorem compl_bihimp_compl : aᶜaᶜ ⇔ bᶜ = a ⇔ b :=
  @compl_symmDiff_compl αᵒᵈ _ _ _

Bi-implication Invariance Under Complementation: $a^c \Leftrightarrow b^c = a \Leftrightarrow b$

Informal description

For any elements $a$ and $b$ in a bi-Heyting algebra, the bi-implication of their complements equals the bi-implication of the original elements, i.e., $a^c \Leftrightarrow b^c = a \Leftrightarrow b$.

symmDiff_eq_top theorem

: a ∆ b = ⊤ ↔ IsCompl a b

Full source

@[simp]
theorem symmDiff_eq_top : a ∆ ba ∆ b = ⊤ ↔ IsCompl a b := by
  rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff,
    codisjoint_iff, and_comm]

Symmetric Difference Equals Top iff Elements Are Complements: $a \triangle b = \top \leftrightarrow \text{IsCompl}(a, b)$

Informal description

For any elements $a$ and $b$ in a co-Heyting algebra, the symmetric difference $a \triangle b$ equals the top element $\top$ if and only if $a$ and $b$ are complements of each other (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$).

bihimp_eq_bot theorem

: a ⇔ b = ⊥ ↔ IsCompl a b

Full source

@[simp]
theorem bihimp_eq_bot : a ⇔ ba ⇔ b = ⊥ ↔ IsCompl a b := by
  rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
    codisjoint_iff]

Bi-implication Equals Bottom iff Elements Are Complements: $a \Leftrightarrow b = \bot \leftrightarrow \text{IsCompl}(a, b)$

Informal description

For any elements $a$ and $b$ in a bi-Heyting algebra, the bi-implication $a \Leftrightarrow b$ equals the bottom element $\bot$ if and only if $a$ and $b$ are complements of each other (i.e., $a \sqcup b = \top$ and $a \sqcap b = \bot$).

compl_symmDiff_self theorem

: aᶜ ∆ a = ⊤

Full source

@[simp]
theorem compl_symmDiff_self : aᶜaᶜ ∆ a = ⊤ :=
  hnot_symmDiff_self _

Symmetric Difference of Complement and Element is Top: $a^c \mathbin{∆} a = \top$

Informal description

In a co-Heyting algebra $\alpha$, for any element $a \in \alpha$, the symmetric difference between the complement $a^c$ and $a$ equals the top element $\top$, i.e., $a^c \mathbin{∆} a = \top$.

symmDiff_compl_self theorem

: a ∆ aᶜ = ⊤

Full source

@[simp]
theorem symmDiff_compl_self : a ∆ aᶜ = ⊤ :=
  symmDiff_hnot_self _

Symmetric Difference with Complement Yields Top: $a \mathbin{∆} a^c = \top$

Informal description

For any element $a$ in a co-Heyting algebra, the symmetric difference between $a$ and its complement $a^c$ equals the top element $\top$, i.e., $a \mathbin{∆} a^c = \top$.

symmDiff_symmDiff_right' theorem

: a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c

Full source

theorem symmDiff_symmDiff_right' :
    a ∆ (b ∆ c) = a ⊓ ba ⊓ b ⊓ ca ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c :=
  calc
    a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ)a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ := by
        { rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq] }
    _ = a ⊓ ba ⊓ b ⊓ ca ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ := by
        { rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc] }
    _ = a ⊓ ba ⊓ b ⊓ ca ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜa ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c := (by
      congr 1
      · congr 1
        rw [inf_comm, inf_assoc]
      · apply inf_left_right_swap)

Associativity-like Identity for Symmetric Difference: $a \mathbin{∆} (b \mathbin{∆} c) = \text{(four-term expression)}$

Informal description

In a bi-Heyting algebra, the symmetric difference operation satisfies the following associativity-like identity: $$ a \mathbin{∆} (b \mathbin{∆} c) = (a \sqcap b \sqcap c) \sqcup (a \sqcap b^c \sqcap c^c) \sqcup (a^c \sqcap b \sqcap c^c) \sqcup (a^c \sqcap b^c \sqcap c). $$ Here $∆$ denotes the symmetric difference operation, $\sqcap$ is the meet operation, $\sqcup$ is the join operation, and $a^c$ denotes the complement of $a$.

Disjoint.le_symmDiff_sup_symmDiff_left theorem

(h : Disjoint a b) : c ≤ a ∆ c ⊔ b ∆ c

Full source

theorem Disjoint.le_symmDiff_sup_symmDiff_left (h : Disjoint a b) : c ≤ a ∆ ca ∆ c ⊔ b ∆ c := by
  trans c \ (a ⊓ b)
  · rw [h.eq_bot, sdiff_bot]
  · rw [sdiff_inf]
    exact sup_le_sup le_sup_right le_sup_right

Disjointness Implies $c \leq (a \Delta c) \sqcup (b \Delta c)$

Informal description

For any elements $a, b, c$ in a bi-Heyting algebra, if $a$ and $b$ are disjoint (i.e., $a \sqcap b = \bot$), then $c$ is less than or equal to the supremum of the symmetric differences $a \Delta c$ and $b \Delta c$, i.e., $$c \leq (a \Delta c) \sqcup (b \Delta c).$$

Disjoint.le_symmDiff_sup_symmDiff_right theorem

(h : Disjoint b c) : a ≤ a ∆ b ⊔ a ∆ c

Full source

theorem Disjoint.le_symmDiff_sup_symmDiff_right (h : Disjoint b c) : a ≤ a ∆ ba ∆ b ⊔ a ∆ c := by
  simp_rw [symmDiff_comm a]
  exact h.le_symmDiff_sup_symmDiff_left

Disjointness Implies $a \leq (a \Delta b) \sqcup (a \Delta c)$

Informal description

For any elements $a, b, c$ in a bi-Heyting algebra, if $b$ and $c$ are disjoint (i.e., $b \sqcap c = \bot$), then $a$ is less than or equal to the supremum of the symmetric differences $a \Delta b$ and $a \Delta c$, i.e., $$a \leq (a \Delta b) \sqcup (a \Delta c).$$

Codisjoint.bihimp_inf_bihimp_le_left theorem

(h : Codisjoint a b) : a ⇔ c ⊓ b ⇔ c ≤ c

Full source

theorem Codisjoint.bihimp_inf_bihimp_le_left (h : Codisjoint a b) : a ⇔ ca ⇔ c ⊓ b ⇔ c ≤ c :=
  h.dual.le_symmDiff_sup_symmDiff_left

Codisjointness Implies $(a \Leftrightarrow c) \sqcap (b \Leftrightarrow c) \leq c$ in Bi-Heyting Algebras

Informal description

For any elements $a, b, c$ in a bi-Heyting algebra, if $a$ and $b$ are codisjoint (i.e., $a \sqcup b = \top$), then the infimum of the bi-implications $a \Leftrightarrow c$ and $b \Leftrightarrow c$ is less than or equal to $c$, i.e., $$(a \Leftrightarrow c) \sqcap (b \Leftrightarrow c) \leq c.$$

Codisjoint.bihimp_inf_bihimp_le_right theorem

(h : Codisjoint b c) : a ⇔ b ⊓ a ⇔ c ≤ a

Full source

theorem Codisjoint.bihimp_inf_bihimp_le_right (h : Codisjoint b c) : a ⇔ ba ⇔ b ⊓ a ⇔ c ≤ a :=
  h.dual.le_symmDiff_sup_symmDiff_right

Codisjointness Implies $(a \Leftrightarrow b) \sqcap (a \Leftrightarrow c) \leq a$ in Bi-Heyting Algebras

Informal description

For any elements $a, b, c$ in a bi-Heyting algebra, if $b$ and $c$ are codisjoint (i.e., $b \sqcup c = \top$), then the infimum of the bi-implications $a \Leftrightarrow b$ and $a \Leftrightarrow c$ is less than or equal to $a$, i.e., $$(a \Leftrightarrow b) \sqcap (a \Leftrightarrow c) \leq a.$$

symmDiff_fst theorem

[GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) : (a ∆ b).1 = a.1 ∆ b.1

Full source

@[simp]
theorem symmDiff_fst [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β]
    (a b : α × β) : (a ∆ b).1 = a.1 ∆ b.1 :=
  rfl

First Component of Symmetric Difference in Product Algebra

Informal description

Let $\alpha$ and $\beta$ be generalized co-Heyting algebras. For any pairs $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in $\alpha \times \beta$, the first component of their symmetric difference $a \Delta b$ equals the symmetric difference of their first components, i.e., $(a \Delta b)_1 = a_1 \Delta b_1$.

symmDiff_snd theorem

[GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) : (a ∆ b).2 = a.2 ∆ b.2

Full source

@[simp]
theorem symmDiff_snd [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β]
    (a b : α × β) : (a ∆ b).2 = a.2 ∆ b.2 :=
  rfl

Second Component of Symmetric Difference in Product Algebra

Informal description

Let $\alpha$ and $\beta$ be generalized co-Heyting algebras. For any pairs $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product algebra $\alpha \times \beta$, the second component of their symmetric difference $a \Delta b$ equals the symmetric difference of their second components, i.e., $(a \Delta b)_2 = a_2 \Delta b_2$.

bihimp_fst theorem

[GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) : (a ⇔ b).1 = a.1 ⇔ b.1

Full source

@[simp]
theorem bihimp_fst [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) :
    (a ⇔ b).1 = a.1 ⇔ b.1 :=
  rfl

First Component of Bi-Implication in Product Algebra

Informal description

Let $\alpha$ and $\beta$ be generalized Heyting algebras. For any pairs $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product algebra $\alpha \times \beta$, the first component of their bi-implication $a \Leftrightarrow b$ equals the bi-implication of their first components, i.e., $(a \Leftrightarrow b)_1 = a_1 \Leftrightarrow b_1$.

bihimp_snd theorem

[GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) : (a ⇔ b).2 = a.2 ⇔ b.2

Full source

@[simp]
theorem bihimp_snd [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) :
    (a ⇔ b).2 = a.2 ⇔ b.2 :=
  rfl

Second Component of Bi-Implication in Product Algebra

Informal description

Let $\alpha$ and $\beta$ be generalized Heyting algebras. For any pairs $a = (a_1, a_2)$ and $b = (b_1, b_2)$ in the product algebra $\alpha \times \beta$, the second component of their bi-implication $a \Leftrightarrow b$ equals the bi-implication of their second components, i.e., $(a \Leftrightarrow b)_2 = a_2 \Leftrightarrow b_2$.

Pi.symmDiff_def theorem

[∀ i, GeneralizedCoheytingAlgebra (π i)] (a b : ∀ i, π i) : a ∆ b = fun i => a i ∆ b i

Full source

theorem symmDiff_def [∀ i, GeneralizedCoheytingAlgebra (π i)] (a b : ∀ i, π i) :
    a ∆ b = fun i => a i ∆ b i :=
  rfl

Pointwise Symmetric Difference in Product of Generalized Co-Heyting Algebras

Informal description

For any family of generalized co-Heyting algebras $(\pi_i)_{i \in \iota}$ and any two functions $a, b \in \prod_{i \in \iota} \pi_i$, the symmetric difference $a \Delta b$ is the function defined pointwise by $(a \Delta b)(i) = a(i) \Delta b(i)$ for each $i \in \iota$.

Pi.bihimp_def theorem

[∀ i, GeneralizedHeytingAlgebra (π i)] (a b : ∀ i, π i) : a ⇔ b = fun i => a i ⇔ b i

Full source

theorem bihimp_def [∀ i, GeneralizedHeytingAlgebra (π i)] (a b : ∀ i, π i) :
    a ⇔ b = fun i => a i ⇔ b i :=
  rfl

Pointwise Bi-Implication in Product of Generalized Heyting Algebras

Informal description

For any family of generalized Heyting algebras $(\pi_i)_{i \in \iota}$ and any two elements $a, b \in \prod_{i \in \iota} \pi_i$, the bi-implication $a \Leftrightarrow b$ is the function defined pointwise by $(a \Leftrightarrow b)(i) = a(i) \Leftrightarrow b(i)$ for each $i \in \iota$.

Pi.symmDiff_apply theorem

[∀ i, GeneralizedCoheytingAlgebra (π i)] (a b : ∀ i, π i) (i : ι) : (a ∆ b) i = a i ∆ b i

Full source

@[simp]
theorem symmDiff_apply [∀ i, GeneralizedCoheytingAlgebra (π i)] (a b : ∀ i, π i) (i : ι) :
    (a ∆ b) i = a i ∆ b i :=
  rfl

Pointwise Symmetric Difference in Product of Generalized Co-Heyting Algebras

Informal description

For any family of generalized co-Heyting algebras $(\pi_i)_{i \in \iota}$ and any two functions $a, b \in \prod_{i \in \iota} \pi_i$, the symmetric difference evaluated at any index $i \in \iota$ satisfies $(a \Delta b)(i) = a(i) \Delta b(i)$.

Pi.bihimp_apply theorem

[∀ i, GeneralizedHeytingAlgebra (π i)] (a b : ∀ i, π i) (i : ι) : (a ⇔ b) i = a i ⇔ b i

Full source

@[simp]
theorem bihimp_apply [∀ i, GeneralizedHeytingAlgebra (π i)] (a b : ∀ i, π i) (i : ι) :
    (a ⇔ b) i = a i ⇔ b i :=
  rfl

Pointwise Bi-implication in Product of Generalized Heyting Algebras

Informal description

For any family of generalized Heyting algebras $\{\pi_i\}_{i \in \iota}$ and any two elements $a, b \in \prod_{i \in \iota} \pi_i$, the bi-implication operation evaluated at any index $i \in \iota$ satisfies $(a \Leftrightarrow b)(i) = a(i) \Leftrightarrow b(i)$, where $\Leftrightarrow$ denotes the bi-implication operation in each $\pi_i$.

Mathlib.Order.SymmDiff

Examples

Main declarations

Notations

References

Tags