/-
Copyright (c) 2021 Bryan Gin-ge Chen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Topaz, Bryan Gin-ge Chen, Yaël Dillies
Ported by: Frédéric Dupuis

! This file was ported from Lean 3 source module order.symm_diff
! leanprover-community/mathlib commit 6eb334bd8f3433d5b08ba156b8ec3e6af47e1904
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.BooleanAlgebra
import Mathlib.Logic.Equiv.Basic

/-!
# Symmetric difference and bi-implication

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

## Examples

Some examples are
* The symmetric difference of two sets is the set of elements that are in either but not both.
* The symmetric difference on propositions is `Xor'`.
* The symmetric difference on `Bool` is `Bool.xor`.
* The equivalence of propositions. Two propositions are equivalent if they imply each other.
* The symmetric difference translates to addition when considering a Boolean algebra as a Boolean
  ring.

## Main declarations

* `symmDiff`: The symmetric difference operator, defined as `(a \ b) ⊔ (b \ a)`
* `bihimp`: The bi-implication operator, defined as `(b ⇨ a) ⊓ (a ⇨ b)`

In generalized Boolean algebras, the symmetric difference operator is:

* `symmDiff_comm`: commutative, and
* `symmDiff_assoc`: associative.

## Notations

* `a ∆ b`: `symmDiff a b`
* `a ⇔ b`: `bihimp a b`

## References

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

* 

## Tags

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


open Function OrderDual

variable {ι: Type ?u.62901
ι α: Type ?u.5
α β: Type ?u.62907
β : Type _: Type (?u.78448+1)
Type _} {π: ι → Type ?u.13
π : ι: Type ?u.16
ι → Type _: Type (?u.32974+1)
Type _}

/-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/
def symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff [Sup: Type ?u.30 → Type ?u.30
Sup α: Type ?u.19
α] [SDiff: Type ?u.33 → Type ?u.33
SDiff α: Type ?u.19
α] (a: α
a b: α
b : α: Type ?u.19
α) : α: Type ?u.19
α :=
  a: α
a \ b: α
b ⊔ b: α
b \ a: α
a
#align symm_diff symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff

/-- The Heyting bi-implication is `(b ⇨ a) ⊓ (a ⇨ b)`. This generalizes equivalence of
propositions. -/
def bihimp: [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp [Inf: Type ?u.189 → Type ?u.189
Inf α: Type ?u.178
α] [HImp: Type ?u.192 → Type ?u.192
HImp α: Type ?u.178
α] (a: α
a b: α
b : α: Type ?u.178
α) : α: Type ?u.178
α :=
  (b: α
b ⇨ a: α
a) ⊓ (a: α
a ⇨ b: α
b)
#align bihimp bihimp: {α : Type u_1} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp

/- This notation might conflict with the Laplacian once we have it. Feel free to put it in locale
  `order` or `symmDiff` if that happens. -/
/-- Notation for symmDiff -/
infixl:100 " ∆ " =>  symmDiff: {α : Type u_1} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff

/-- Notation for bihimp -/
infixl:100 " ⇔ " => bihimp: {α : Type u_1} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp

theorem symmDiff_def: ∀ {α : Type u_1} [inst : Sup α] [inst_1 : SDiff α] (a b : α), a ∆ b = a \ b ⊔ b \ a
symmDiff_def [Sup: Type ?u.15945 → Type ?u.15945
Sup α: Type ?u.15934
α] [SDiff: Type ?u.15948 → Type ?u.15948
SDiff α: Type ?u.15934
α] (a: α
a b: α
b : α: Type ?u.15934
α) : a: α
a ∆ b: α
b = a: α
a \ b: α
b ⊔ b: α
b \ a: α
a :=
  rfl: ∀ {α : Sort ?u.16008} {a : α}, a = a
rfl
#align symm_diff_def symmDiff_def: ∀ {α : Type u_1} [inst : Sup α] [inst_1 : SDiff α] (a b : α), a ∆ b = a \ b ⊔ b \ a
symmDiff_def

theorem bihimp_def: ∀ [inst : Inf α] [inst_1 : HImp α] (a b : α), a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)
bihimp_def [Inf: Type ?u.16034 → Type ?u.16034
Inf α: Type ?u.16023
α] [HImp: Type ?u.16037 → Type ?u.16037
HImp α: Type ?u.16023
α] (a: α
a b: α
b : α: Type ?u.16023
α) : a: α
a ⇔ b: α
b = (b: α
b ⇨ a: α
a) ⊓ (a: α
a ⇨ b: α
b) :=
  rfl: ∀ {α : Sort ?u.16090} {a : α}, a = a
rfl
#align bihimp_def bihimp_def: ∀ {α : Type u_1} [inst : Inf α] [inst_1 : HImp α] (a b : α), a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)
bihimp_def

theorem symmDiff_eq_Xor': ∀ (p q : Prop), p ∆ q = Xor' p q
symmDiff_eq_Xor' (p: Prop
p q: Prop
q : Prop: Type
Prop) : p: Prop
p ∆ q: Prop
q = Xor': Prop → Prop → Prop
Xor' p: Prop
p q: Prop
q :=
  rfl: ∀ {α : Sort ?u.16215} {a : α}, a = a
rfl
#align symm_diff_eq_xor symmDiff_eq_Xor': ∀ (p q : Prop), p ∆ q = Xor' p q
symmDiff_eq_Xor'

@[simp]
theorem bihimp_iff_iff: ∀ {p q : Prop}, p ⇔ q ↔ (p ↔ q)
bihimp_iff_iff {p: Prop
p q: Prop
q : Prop: Type
Prop} : p: Prop
p ⇔ q: Prop
q ↔ (p: Prop
p ↔ q: Prop
q) :=
  (iff_iff_implies_and_implies: ∀ (a b : Prop), (a ↔ b) ↔ (a → b) ∧ (b → a)
iff_iff_implies_and_implies _: Prop
_ _: Prop
_).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans Iff.comm: ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)
Iff.comm
#align bihimp_iff_iff bihimp_iff_iff: ∀ {p q : Prop}, p ⇔ q ↔ (p ↔ q)
bihimp_iff_iff

@[simp]
theorem Bool.symmDiff_eq_xor: ∀ (p q : Bool), p ∆ q = xor p q
Bool.symmDiff_eq_xor : ∀ p: Bool
p q: Bool
q : Bool: Type
Bool, p: Bool
p ∆ q: Bool
q = xor: Bool → Bool → Bool
xor p: Bool
p q: Bool
q := by
Goals accomplished! 🐙 ι: Type ?u.16365

α: Type ?u.16368

β: Type ?u.16371

π: ι → Type ?u.16376

∀ (p q : Bool), p ∆ q = xor p qdecide
Goals accomplished! 🐙
#align bool.symm_diff_eq_bxor Bool.symmDiff_eq_xor: ∀ (p q : Bool), p ∆ q = xor p q
Bool.symmDiff_eq_xor

section GeneralizedCoheytingAlgebra

variable [GeneralizedCoheytingAlgebra: Type ?u.18827 → Type ?u.18827
GeneralizedCoheytingAlgebra α: Type ?u.16635
α] (a: α
a b: α
b c: α
c d: α
d : α: Type ?u.26727
α)

@[simp]
theorem toDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), ↑toDual (a ∆ b) = ↑toDual a ⇔ ↑toDual b
toDual_symmDiff : toDual: {α : Type ?u.16658} → α ≃ αᵒᵈ
toDual (a: α
a ∆ b: α
b) = toDual: {α : Type ?u.16804} → α ≃ αᵒᵈ
toDual a: α
a ⇔ toDual: {α : Type ?u.16869} → α ≃ αᵒᵈ
toDual b: α
b :=
  rfl: ∀ {α : Sort ?u.16986} {a : α}, a = a
rfl
#align to_dual_symm_diff toDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), ↑toDual (a ∆ b) = ↑toDual a ⇔ ↑toDual b
toDual_symmDiff

@[simp]
theorem ofDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ⇔ b) = ↑ofDual a ∆ ↑ofDual b
ofDual_bihimp (a: αᵒᵈ
a b: αᵒᵈ
b : α: Type ?u.17036
αᵒᵈ) : ofDual: {α : Type ?u.17065} → αᵒᵈ ≃ α
ofDual (a: αᵒᵈ
a ⇔ b: αᵒᵈ
b) = ofDual: {α : Type ?u.17217} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a ∆ ofDual: {α : Type ?u.17282} → αᵒᵈ ≃ α
ofDual b: αᵒᵈ
b :=
  rfl: ∀ {α : Sort ?u.17411} {a : α}, a = a
rfl
#align of_dual_bihimp ofDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ⇔ b) = ↑ofDual a ∆ ↑ofDual b
ofDual_bihimp

theorem symmDiff_comm: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm : a: α
a ∆ b: α
b = b: α
b ∆ a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.17458

α: Type u_1

β: Type ?u.17464

π: ι → Type ?u.17469

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b = b ∆ asimp only [symmDiff: {α : Type ?u.17557} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff, sup_comm: ∀ {α : Type ?u.17564} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ a
sup_comm]
Goals accomplished! 🐙
#align symm_diff_comm symmDiff_comm: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm

instance symmDiff_isCommutative: IsCommutative α fun x x_1 => x ∆ x_1
symmDiff_isCommutative : IsCommutative: (α : Type ?u.17728) → (α → α → α) → Prop
IsCommutative α: Type ?u.17706
α (· ∆ ·): α → α → α
(· ∆ ·) :=
  ⟨symmDiff_comm: ∀ {α : Type ?u.17833} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm⟩
#align symm_diff_is_comm symmDiff_isCommutative: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α], IsCommutative α fun x x_1 => x ∆ x_1
symmDiff_isCommutative

@[simp]
theorem symmDiff_self: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ a = ⊥
symmDiff_self : a: α
a ∆ a: α
a = ⊥: ?m.17971
⊥ := by
Goals accomplished! 🐙 ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ a = ⊥rw [ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ a = ⊥symmDiff: {α : Type ?u.18160} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ a ⊔ a \ a = ⊥ ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ a = ⊥sup_idem: ∀ {α : Type ?u.18161} [inst : SemilatticeSup α] {a : α}, a ⊔ a = a
sup_idem,ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ a = ⊥ ι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ a = ⊥sdiff_self: ∀ {α : Type ?u.18207} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ a = ⊥
sdiff_selfι: Type ?u.17889

α: Type u_1

β: Type ?u.17895

π: ι → Type ?u.17900

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

⊥ = ⊥]
Goals accomplished! 🐙
#align symm_diff_self symmDiff_self: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ a = ⊥
symmDiff_self

@[simp]
theorem symmDiff_bot: a ∆ ⊥ = a
symmDiff_bot : a: α
a ∆ ⊥: ?m.18291
⊥ = a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = arw [ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = asymmDiff: {α : Type ?u.18505} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ ⊥ ⊔ ⊥ \ a = a ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = asdiff_bot: ∀ {α : Type ?u.18506} [inst : GeneralizedCoheytingAlgebra α] {a : α}, a \ ⊥ = a
sdiff_bot,ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ ⊥ \ a = a ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = abot_sdiff: ∀ {α : Type ?u.18541} [inst : GeneralizedCoheytingAlgebra α] {a : α}, ⊥ \ a = ⊥
bot_sdiff,ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ ⊥ = a ι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = asup_bot_eq: ∀ {α : Type ?u.18567} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, a ⊔ ⊥ = a
sup_bot_eqι: Type ?u.18260

α: Type u_1

β: Type ?u.18266

π: ι → Type ?u.18271

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a = a]
Goals accomplished! 🐙
#align symm_diff_bot symmDiff_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ ⊥ = a
symmDiff_bot

@[simp]
theorem bot_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), ⊥ ∆ a = a
bot_symmDiff : ⊥: ?m.18844
⊥ ∆ a: α
a = a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.18813

α: Type u_1

β: Type ?u.18819

π: ι → Type ?u.18824

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

⊥ ∆ a = arw [ι: Type ?u.18813

α: Type u_1

β: Type ?u.18819

π: ι → Type ?u.18824

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

⊥ ∆ a = asymmDiff_comm: ∀ {α : Type ?u.18962} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm,ι: Type ?u.18813

α: Type u_1

β: Type ?u.18819

π: ι → Type ?u.18824

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ ⊥ = a ι: Type ?u.18813

α: Type u_1

β: Type ?u.18819

π: ι → Type ?u.18824

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

⊥ ∆ a = asymmDiff_bot: ∀ {α : Type ?u.18999} [inst : GeneralizedCoheytingAlgebra α] (a : α), a ∆ ⊥ = a
symmDiff_botι: Type ?u.18813

α: Type u_1

β: Type ?u.18819

π: ι → Type ?u.18824

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a = a]
Goals accomplished! 🐙
#align bot_symm_diff bot_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a : α), ⊥ ∆ a = a
bot_symmDiff

@[simp]
theorem symmDiff_eq_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = b
symmDiff_eq_bot {a: α
a b: α
b : α: Type ?u.19060
α} : a: α
a ∆ b: α
b = ⊥: ?m.19143
⊥ ↔ a: α
a = b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ∆ b = ⊥ ↔ a = bsimp_rw [ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ∆ b = ⊥ ↔ a = bsymmDiff: {α : Type ?u.19309} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a \ b ⊔ b \ a = ⊥ ↔ a = b ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ∆ b = ⊥ ↔ a = bsup_eq_bot_iff: ∀ {α : Type ?u.19439} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a b : α}, a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
sup_eq_bot_iff,ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a \ b = ⊥ ∧ b \ a = ⊥ ↔ a = b ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ∆ b = ⊥ ↔ a = bsdiff_eq_bot_iff: ∀ {α : Type ?u.19723} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ b
sdiff_eq_bot_iff,ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ≤ b ∧ b ≤ a ↔ a = b ι: Type ?u.19057

α: Type u_1

β: Type ?u.19063

π: ι → Type ?u.19068

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

a ∆ b = ⊥ ↔ a = ble_antisymm_iff: ∀ {α : Type ?u.19890} [inst : PartialOrder α] {a b : α}, a = b ↔ a ≤ b ∧ b ≤ a
le_antisymm_iff
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align symm_diff_eq_bot symmDiff_eq_bot: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = b
symmDiff_eq_bot

theorem symmDiff_of_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ∆ b = b \ a
symmDiff_of_le {a: α
a b: α
b : α: Type ?u.20050
α} (h: a ≤ b
h : a: α
a ≤ b: α
b) : a: α
a ∆ b: α
b = b: α
b \ a: α
a := by
Goals accomplished! 🐙
  ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ∆ b = b \ arw [ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ∆ b = b \ asymmDiff: {α : Type ?u.20290} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a \ b ⊔ b \ a = b \ a ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ∆ b = b \ asdiff_eq_bot_iff: ∀ {α : Type ?u.20291} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ b
sdiff_eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: a ≤ b
h,ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

⊥ ⊔ b \ a = b \ a ι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ∆ b = b \ abot_sup_eq: ∀ {α : Type ?u.20341} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, ⊥ ⊔ a = a
bot_sup_eqι: Type ?u.20047

α: Type u_1

β: Type ?u.20053

π: ι → Type ?u.20058

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

b \ a = b \ a]
Goals accomplished! 🐙
#align symm_diff_of_le symmDiff_of_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ∆ b = b \ a
symmDiff_of_le

theorem symmDiff_of_ge: ∀ {a b : α}, b ≤ a → a ∆ b = a \ b
symmDiff_of_ge {a: α
a b: α
b : α: Type ?u.20572
α} (h: b ≤ a
h : b: α
b ≤ a: α
a) : a: α
a ∆ b: α
b = a: α
a \ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ∆ b = a \ brw [ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ∆ b = a \ bsymmDiff: {α : Type ?u.20812} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a \ b ⊔ b \ a = a \ b ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ∆ b = a \ bsdiff_eq_bot_iff: ∀ {α : Type ?u.20813} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b = ⊥ ↔ a ≤ b
sdiff_eq_bot_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: b ≤ a
h,ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a \ b ⊔ ⊥ = a \ b ι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ∆ b = a \ bsup_bot_eq: ∀ {α : Type ?u.20863} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, a ⊔ ⊥ = a
sup_bot_eqι: Type ?u.20569

α: Type u_1

β: Type ?u.20575

π: ι → Type ?u.20580

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a \ b = a \ b]
Goals accomplished! 🐙
#align symm_diff_of_ge symmDiff_of_ge: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b ≤ a → a ∆ b = a \ b
symmDiff_of_ge

theorem symmDiff_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ∆ b ≤ c
symmDiff_le {a: α
a b: α
b c: α
c : α: Type ?u.21094
α} (ha: a ≤ b ⊔ c
ha : a: α
a ≤ b: α
b ⊔ c: α
c) (hb: b ≤ a ⊔ c
hb : b: α
b ≤ a: α
a ⊔ c: α
c) : a: α
a ∆ b: α
b ≤ c: α
c :=
  sup_le: ∀ {α : Type ?u.21238} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
sup_le (sdiff_le_iff: ∀ {α : Type ?u.21288} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ c
sdiff_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 ha: a ≤ b ⊔ c
ha) <| sdiff_le_iff: ∀ {α : Type ?u.21324} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ c
sdiff_le_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hb: b ≤ a ⊔ c
hb
#align symm_diff_le symmDiff_le: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ≤ b ⊔ c → b ≤ a ⊔ c → a ∆ b ≤ c
symmDiff_le

theorem symmDiff_le_iff: ∀ {a b c : α}, a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
symmDiff_le_iff {a: α
a b: α
b c: α
c : α: Type ?u.21358
α} : a: α
a ∆ b: α
b ≤ c: α
c ↔ a: α
a ≤ b: α
b ⊔ c: α
c ∧ b: α
b ≤ a: α
a ⊔ c: α
c := by
Goals accomplished! 🐙
  ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csimp_rw [ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csymmDiff: {α : Type ?u.21606} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a \ b ⊔ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csup_le_iff: ∀ {α : Type ?u.21700} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
sup_le_iff,ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a \ b ≤ c ∧ b \ a ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c ι: Type ?u.21355

α: Type u_1

β: Type ?u.21361

π: ι → Type ?u.21366

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ csdiff_le_iff: ∀ {α : Type ?u.21874} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a \ b ≤ c ↔ a ≤ b ⊔ c
sdiff_le_iff
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align symm_diff_le_iff symmDiff_le_iff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
symmDiff_le_iff

@[simp]
theorem symmDiff_le_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ b
symmDiff_le_sup {a: α
a b: α
b : α: Type ?u.22046
α} : a: α
a ∆ b: α
b ≤ a: α
a ⊔ b: α
b :=
  sup_le_sup: ∀ {α : Type ?u.22169} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
sup_le_sup sdiff_le: ∀ {α : Type ?u.22220} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
sdiff_le sdiff_le: ∀ {α : Type ?u.22249} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
sdiff_le
#align symm_diff_le_sup symmDiff_le_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ b
symmDiff_le_sup

theorem symmDiff_eq_sup_sdiff_inf: a ∆ b = (a ⊔ b) \ (a ⊓ b)
symmDiff_eq_sup_sdiff_inf : a: α
a ∆ b: α
b = (a: α
a ⊔ b: α
b) \ (a: α
a ⊓ b: α
b) := by
Goals accomplished! 🐙 ι: Type ?u.22302

α: Type u_1

β: Type ?u.22308

π: ι → Type ?u.22313

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b = (a ⊔ b) \ (a ⊓ b)simp [sup_sdiff: ∀ {α : Type ?u.22435} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a ⊔ b) \ c = a \ c ⊔ b \ c
sup_sdiff, symmDiff: {α : Type ?u.22455} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff]
Goals accomplished! 🐙
#align symm_diff_eq_sup_sdiff_inf symmDiff_eq_sup_sdiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = (a ⊔ b) \ (a ⊓ b)
symmDiff_eq_sup_sdiff_inf

theorem Disjoint.symmDiff_eq_sup: ∀ {a b : α}, Disjoint a b → a ∆ b = a ⊔ b
Disjoint.symmDiff_eq_sup {a: α
a b: α
b : α: Type ?u.26275
α} (h: Disjoint a b
h : Disjoint: {α : Type ?u.26301} → [inst : PartialOrder α] → [inst : OrderBot α] → α → α → Prop
Disjoint a: α
a b: α
b) : a: α
a ∆ b: α
b = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ∆ b = a ⊔ brw [ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ∆ b = a ⊔ bsymmDiff: {α : Type ?u.26662} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a \ b ⊔ b \ a = a ⊔ b ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ∆ b = a ⊔ bh: Disjoint a b
h.sdiff_eq_left: ∀ {α : Type ?u.26663} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a \ b = a
sdiff_eq_left,ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ⊔ b \ a = a ⊔ b ι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ∆ b = a ⊔ bh: Disjoint a b
h.sdiff_eq_right: ∀ {α : Type ?u.26696} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → b \ a = b
sdiff_eq_rightι: Type ?u.26272

α: Type u_1

β: Type ?u.26278

π: ι → Type ?u.26283

inst✝: GeneralizedCoheytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Disjoint a b

a ⊔ b = a ⊔ b]
Goals accomplished! 🐙
#align disjoint.symm_diff_eq_sup Disjoint.symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, Disjoint a b → a ∆ b = a ⊔ b
Disjoint.symmDiff_eq_sup

theorem symmDiff_sdiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
symmDiff_sdiff : a: α
a ∆ b: α
b \ c: α
c = a: α
a \ (b: α
b ⊔ c: α
c) ⊔ b: α
b \ (a: α
a ⊔ c: α
c) := by
Goals accomplished! 🐙
  ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)rw [ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)symmDiff: {α : Type ?u.27010} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b ⊔ b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sup_sdiff_distrib: ∀ {α : Type ?u.27011} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), (a ⊔ b) \ c = a \ c ⊔ b \ c
sup_sdiff_distrib,ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b) \ c ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sdiff_sdiff_left: ∀ {α : Type ?u.27053} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)
sdiff_sdiff_left,ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b ⊔ c) ⊔ (b \ a) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)sdiff_sdiff_left: ∀ {α : Type ?u.27081} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, (a \ b) \ c = a \ (b ⊔ c)
sdiff_sdiff_leftι: Type ?u.26724

α: Type u_1

β: Type ?u.26730

π: ι → Type ?u.26735

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b ⊔ c) ⊔ b \ (a ⊔ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)]
Goals accomplished! 🐙
#align symm_diff_sdiff symmDiff_sdiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
symmDiff_sdiff

@[simp]
theorem symmDiff_sdiff_inf: a ∆ b \ (a ⊓ b) = a ∆ b
symmDiff_sdiff_inf : a: α
a ∆ b: α
b \ (a: α
a ⊓ b: α
b) = a: α
a ∆ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.27143

α: Type u_1

β: Type ?u.27149

π: ι → Type ?u.27154

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ (a ⊓ b) = a ∆ brw [ι: Type ?u.27143

α: Type u_1

β: Type ?u.27149

π: ι → Type ?u.27154

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ (a ⊓ b) = a ∆ bsymmDiff_sdiff: ∀ {α : Type ?u.27289} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
symmDiff_sdiffι: Type ?u.27143

α: Type u_1

β: Type ?u.27149

π: ι → Type ?u.27154

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b]ι: Type ?u.27143

α: Type u_1

β: Type ?u.27149

π: ι → Type ?u.27154

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
  ι: Type ?u.27143

α: Type u_1

β: Type ?u.27149

π: ι → Type ?u.27154

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b \ (a ⊓ b) = a ∆ bsimp [symmDiff: {α : Type ?u.27352} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff]
Goals accomplished! 🐙
#align symm_diff_sdiff_inf symmDiff_sdiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b \ (a ⊓ b) = a ∆ b
symmDiff_sdiff_inf

@[simp]
theorem symmDiff_sdiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ b
symmDiff_sdiff_eq_sup : a: α
a ∆ (b: α
b \ a: α
a) = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ (b \ a) = a ⊔ brw [ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ (b \ a) = a ⊔ bsymmDiff: {α : Type ?u.32236} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b \ a) ⊔ (b \ a) \ a = a ⊔ b ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ (b \ a) = a ⊔ bsdiff_idem: ∀ {α : Type ?u.32237} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, (a \ b) \ b = a \ b
sdiff_idemι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b \ a) ⊔ b \ a = a ⊔ b]ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ (b \ a) ⊔ b \ a = a ⊔ b
  ι: Type ?u.32022

α: Type u_1

β: Type ?u.32028

π: ι → Type ?u.32033

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ (b \ a) = a ⊔ bexact
    le_antisymm: ∀ {α : Type ?u.32325} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (sup_le_sup: ∀ {α : Type ?u.32348} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
sup_le_sup sdiff_le: ∀ {α : Type ?u.32413} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
sdiff_le sdiff_le: ∀ {α : Type ?u.32439} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
sdiff_le)
      (sup_le: ∀ {α : Type ?u.32461} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
sup_le le_sdiff_sup: ∀ {α : Type ?u.32485} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
le_sdiff_sup <| le_sdiff_sup: ∀ {α : Type ?u.32511} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
le_sdiff_sup.trans: ∀ {α : Type ?u.32525} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans <| sup_le: ∀ {α : Type ?u.32591} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
sup_le le_sup_right: ∀ {α : Type ?u.32615} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right le_sdiff_sup: ∀ {α : Type ?u.32638} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
le_sdiff_sup)
Goals accomplished! 🐙
#align symm_diff_sdiff_eq_sup symmDiff_sdiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ b
symmDiff_sdiff_eq_sup

@[simp]
theorem sdiff_symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ b
sdiff_symmDiff_eq_sup : (a: α
a \ b: α
b) ∆ b: α
b = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b) ∆ b = a ⊔ brw [ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b) ∆ b = a ⊔ bsymmDiff_comm: ∀ {α : Type ?u.32806} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm,ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

b ∆ (a \ b) = a ⊔ b ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b) ∆ b = a ⊔ bsymmDiff_sdiff_eq_sup: ∀ {α : Type ?u.32843} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ b
symmDiff_sdiff_eq_sup,ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

b ⊔ a = a ⊔ b ι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a \ b) ∆ b = a ⊔ bsup_comm: ∀ {α : Type ?u.32882} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ a
sup_commι: Type ?u.32704

α: Type u_1

β: Type ?u.32710

π: ι → Type ?u.32715

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b = a ⊔ b]
Goals accomplished! 🐙
#align sdiff_symm_diff_eq_sup sdiff_symmDiff_eq_sup: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ b
sdiff_symmDiff_eq_sup

@[simp]
theorem symmDiff_sup_inf: a ∆ b ⊔ a ⊓ b = a ⊔ b
symmDiff_sup_inf : a: α
a ∆ b: α
b ⊔ a: α
a ⊓ b: α
b = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ brefine' le_antisymm: ∀ {α : Type ?u.33108} [inst : PartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
le_antisymm (sup_le: ∀ {α : Type ?u.33131} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
sup_le symmDiff_le_sup: ∀ {α : Type ?u.33200} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b ≤ a ⊔ b
symmDiff_le_sup inf_le_sup: ∀ {α : Type ?u.33232} [inst : Lattice α] {a b : α}, a ⊓ b ≤ a ⊔ b
inf_le_sup) _: ?m.33112 ≤ ?m.33111
_ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
  ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ brw [ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ a ∆ b ⊔ a ⊓ bsup_inf_left: ∀ {α : Type ?u.33274} [inst : DistribLattice α] {x y z : α}, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)
sup_inf_left,ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ (a ∆ b ⊔ a) ⊓ (a ∆ b ⊔ b) ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ a ∆ b ⊔ a ⊓ bsymmDiff: {α : Type ?u.33502} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiffι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)]ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
  ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ brefine' sup_le: ∀ {α : Type ?u.33550} [inst : SemilatticeSup α] {a b c : α}, a ≤ c → b ≤ c → a ⊔ b ≤ c
sup_le (le_inf: ∀ {α : Type ?u.33574} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ c
le_inf le_sup_right: ∀ {α : Type ?u.33610} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right _: ?m.33577 ≤ ?m.33579
_) (le_inf: ∀ {α : Type ?u.33640} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ c
le_inf _: ?m.33643 ≤ ?m.33644
_ le_sup_right: ∀ {α : Type ?u.33665} [inst : SemilatticeSup α] {a b : α}, b ≤ a ⊔ b
le_sup_right)ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b \ a ⊔ b
ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ a
  ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ b·ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b \ a ⊔ b ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b \ a ⊔ b
ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ arw [ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b \ a ⊔ bsup_right_comm: ∀ {α : Type ?u.33688} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ b
sup_right_commι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b ⊔ b \ a]ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b ⊔ b \ a
    ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_1a ≤ a \ b ⊔ b \ a ⊔ bexact le_sup_of_le_left: ∀ {α : Type ?u.33768} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ b
le_sup_of_le_left le_sdiff_sup: ∀ {α : Type ?u.33792} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
le_sdiff_sup
Goals accomplished! 🐙
  ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ b·ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ a ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ arw [ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ asup_assoc: ∀ {α : Type ?u.33822} [inst : SemilatticeSup α] {a b c : α}, a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_assocι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ (b \ a ⊔ a)]ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ (b \ a ⊔ a)
    ι: Type ?u.32963

α: Type u_1

β: Type ?u.32969

π: ι → Type ?u.32974

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

refine'_2b ≤ a \ b ⊔ b \ a ⊔ aexact le_sup_of_le_right: ∀ {α : Type ?u.33899} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ b
le_sup_of_le_right le_sdiff_sup: ∀ {α : Type ?u.33923} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ a \ b ⊔ b
le_sdiff_sup
Goals accomplished! 🐙
#align symm_diff_sup_inf symmDiff_sup_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ b
symmDiff_sup_inf

@[simp]
theorem inf_sup_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ b
inf_sup_symmDiff : a: α
a ⊓ b: α
b ⊔ a: α
a ∆ b: α
b = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙 ι: Type ?u.33973

α: Type u_1

β: Type ?u.33979

π: ι → Type ?u.33984

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊓ b ⊔ a ∆ b = a ⊔ brw [ι: Type ?u.33973

α: Type u_1

β: Type ?u.33979

π: ι → Type ?u.33984

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊓ b ⊔ a ∆ b = a ⊔ bsup_comm: ∀ {α : Type ?u.34118} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ a
sup_comm,ι: Type ?u.33973

α: Type u_1

β: Type ?u.33979

π: ι → Type ?u.33984

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ b ι: Type ?u.33973

α: Type u_1

β: Type ?u.33979

π: ι → Type ?u.33984

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊓ b ⊔ a ∆ b = a ⊔ bsymmDiff_sup_inf: ∀ {α : Type ?u.34170} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ b
symmDiff_sup_infι: Type ?u.33973

α: Type u_1

β: Type ?u.33979

π: ι → Type ?u.33984

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b = a ⊔ b]
Goals accomplished! 🐙
#align inf_sup_symm_diff inf_sup_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ b
inf_sup_symmDiff

@[simp]
theorem symmDiff_symmDiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ b
symmDiff_symmDiff_inf : a: α
a ∆ b: α
b ∆ (a: α
a ⊓ b: α
b) = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ∆ (a ⊓ b) = a ⊔ brw [ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ∆ (a ⊓ b) = a ⊔ b← symmDiff_sdiff_inf: ∀ {α : Type ?u.34395} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b \ (a ⊓ b) = a ∆ b
symmDiff_sdiff_inf a: α
a,ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a ∆ b \ (a ⊓ b)) ∆ (a ⊓ b) = a ⊔ b ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ∆ (a ⊓ b) = a ⊔ bsdiff_symmDiff_eq_sup: ∀ {α : Type ?u.34412} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ b
sdiff_symmDiff_eq_sup,ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ⊔ a ⊓ b = a ⊔ b ι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ∆ (a ⊓ b) = a ⊔ bsymmDiff_sup_inf: ∀ {α : Type ?u.34451} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ b
symmDiff_sup_infι: Type ?u.34249

α: Type u_1

β: Type ?u.34255

π: ι → Type ?u.34260

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b = a ⊔ b]
Goals accomplished! 🐙
#align symm_diff_symm_diff_inf symmDiff_symmDiff_inf: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ b
symmDiff_symmDiff_inf

@[simp]
theorem inf_symmDiff_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
inf_symmDiff_symmDiff : (a: α
a ⊓ b: α
b) ∆ (a: α
a ∆ b: α
b) = a: α
a ⊔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.34523

α: Type u_1

β: Type ?u.34529

π: ι → Type ?u.34534

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a ⊓ b) ∆ (a ∆ b) = a ⊔ brw [ι: Type ?u.34523

α: Type u_1

β: Type ?u.34529

π: ι → Type ?u.34534

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a ⊓ b) ∆ (a ∆ b) = a ⊔ bsymmDiff_comm: ∀ {α : Type ?u.34669} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b = b ∆ a
symmDiff_comm,ι: Type ?u.34523

α: Type u_1

β: Type ?u.34529

π: ι → Type ?u.34534

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ b ∆ (a ⊓ b) = a ⊔ b ι: Type ?u.34523

α: Type u_1

β: Type ?u.34529

π: ι → Type ?u.34534

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

(a ⊓ b) ∆ (a ∆ b) = a ⊔ bsymmDiff_symmDiff_inf: ∀ {α : Type ?u.34706} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ b
symmDiff_symmDiff_infι: Type ?u.34523

α: Type u_1

β: Type ?u.34529

π: ι → Type ?u.34534

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ⊔ b = a ⊔ b]
Goals accomplished! 🐙
#align inf_symm_diff_symm_diff inf_symmDiff_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
inf_symmDiff_symmDiff

theorem symmDiff_triangle: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ c
symmDiff_triangle : a: α
a ∆ c: α
c ≤ a: α
a ∆ b: α
b ⊔ b: α
b ∆ c: α
c := by
Goals accomplished! 🐙
  ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ c ≤ a ∆ b ⊔ b ∆ crefine' (sup_le_sup: ∀ {α : Type ?u.34950} [inst : SemilatticeSup α] {a b c d : α}, a ≤ b → c ≤ d → a ⊔ c ≤ b ⊔ d
sup_le_sup (sdiff_triangle: ∀ {α : Type ?u.34957} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a \ c ≤ a \ b ⊔ b \ c
sdiff_triangle a: α
a b: α
b c: α
c) <| sdiff_triangle: ∀ {α : Type ?u.34986} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a \ c ≤ a \ b ⊔ b \ c
sdiff_triangle _: ?m.34987
_ b: α
b _: ?m.34987
_).trans_eq: ∀ {α : Type ?u.34995} [inst : Preorder α] {a b c : α}, a ≤ b → b = c → a ≤ c
trans_eq _: ?m.35006 = ?m.35007
_ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
  ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a ∆ c ≤ a ∆ b ⊔ b ∆ crw [ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c@sup_comm: ∀ {α : Type ?u.35042} [inst : SemilatticeSup α] {a b : α}, a ⊔ b = b ⊔ a
sup_comm _: Type ?u.35042
_ _ (c: α
c \ b: α
b),ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (b \ a ⊔ c \ b) = a ∆ b ⊔ b ∆ c ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csup_sup_sup_comm: ∀ {α : Type ?u.35113} [inst : SemilatticeSup α] (a b c d : α), a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
sup_sup_sup_comm,ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a ∆ b ⊔ b ∆ c ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csymmDiff: {α : Type ?u.35231} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff,ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ b ∆ c ι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ csymmDiff: {α : Type ?u.35289} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiffι: Type ?u.34775

α: Type u_1

β: Type ?u.34781

π: ι → Type ?u.34786

inst✝: GeneralizedCoheytingAlgebra α

a, b, c, d: α

a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b) = a \ b ⊔ b \ a ⊔ (b \ c ⊔ c \ b)]
Goals accomplished! 🐙
#align symm_diff_triangle symmDiff_triangle: ∀ {α : Type u_1} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ c
symmDiff_triangle

end GeneralizedCoheytingAlgebra

section GeneralizedHeytingAlgebra

variable [GeneralizedHeytingAlgebra: Type ?u.38081 → Type ?u.38081
GeneralizedHeytingAlgebra α: Type ?u.35332
α] (a: α
a b: α
b c: α
c d: α
d : α: Type ?u.35307
α)

@[simp]
theorem toDual_bihimp: ↑toDual (a ⇔ b) = ↑toDual a ∆ ↑toDual b
toDual_bihimp : toDual: {α : Type ?u.35355} → α ≃ αᵒᵈ
toDual (a: α
a ⇔ b: α
b) = toDual: {α : Type ?u.35505} → α ≃ αᵒᵈ
toDual a: α
a ∆ toDual: {α : Type ?u.35570} → α ≃ αᵒᵈ
toDual b: α
b :=
  rfl: ∀ {α : Sort ?u.35714} {a : α}, a = a
rfl
#align to_dual_bihimp toDual_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), ↑toDual (a ⇔ b) = ↑toDual a ∆ ↑toDual b
toDual_bihimp

@[simp]
theorem ofDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ∆ b) = ↑ofDual a ⇔ ↑ofDual b
ofDual_symmDiff (a: αᵒᵈ
a b: αᵒᵈ
b : α: Type ?u.35764
αᵒᵈ) : ofDual: {α : Type ?u.35793} → αᵒᵈ ≃ α
ofDual (a: αᵒᵈ
a ∆ b: αᵒᵈ
b) = ofDual: {α : Type ?u.35973} → αᵒᵈ ≃ α
ofDual a: αᵒᵈ
a ⇔ ofDual: {α : Type ?u.36038} → αᵒᵈ ≃ α
ofDual b: αᵒᵈ
b :=
  rfl: ∀ {α : Sort ?u.36164} {a : α}, a = a
rfl
#align of_dual_symm_diff ofDual_symmDiff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : αᵒᵈ), ↑ofDual (a ∆ b) = ↑ofDual a ⇔ ↑ofDual b
ofDual_symmDiff

theorem bihimp_comm: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ a
bihimp_comm : a: α
a ⇔ b: α
b = b: α
b ⇔ a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.36211

α: Type u_1

β: Type ?u.36217

π: ι → Type ?u.36222

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ b = b ⇔ asimp only [(· ⇔ ·), inf_comm: ∀ {α : Type ?u.36320} [inst : SemilatticeInf α] {a b : α}, a ⊓ b = b ⊓ a
inf_comm]
Goals accomplished! 🐙
#align bihimp_comm bihimp_comm: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ a
bihimp_comm

instance bihimp_isCommutative: IsCommutative α fun x x_1 => x ⇔ x_1
bihimp_isCommutative : IsCommutative: (α : Type ?u.36518) → (α → α → α) → Prop
IsCommutative α: Type ?u.36496
α (· ⇔ ·): α → α → α
(· ⇔ ·) :=
  ⟨bihimp_comm: ∀ {α : Type ?u.36627} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ a
bihimp_comm⟩
#align bihimp_is_comm bihimp_isCommutative: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α], IsCommutative α fun x x_1 => x ⇔ x_1
bihimp_isCommutative

@[simp]
theorem bihimp_self: a ⇔ a = ⊤
bihimp_self : a: α
a ⇔ a: α
a = ⊤: ?m.36766
⊤ := by
Goals accomplished! 🐙 ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ a = ⊤rw [ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ a = ⊤bihimp: {α : Type ?u.36943} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(a ⇨ a) ⊓ (a ⇨ a) = ⊤ ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ a = ⊤inf_idem: ∀ {α : Type ?u.36944} [inst : SemilatticeInf α] {a : α}, a ⊓ a = a
inf_idem,ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ a = ⊤ ι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ a = ⊤himp_self: ∀ {α : Type ?u.37007} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ a = ⊤
himp_selfι: Type ?u.36681

α: Type u_1

β: Type ?u.36687

π: ι → Type ?u.36692

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

⊤ = ⊤]
Goals accomplished! 🐙
#align bihimp_self bihimp_self: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ a = ⊤
bihimp_self

@[simp]
theorem bihimp_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = a
bihimp_top : a: α
a ⇔ ⊤: ?m.37088
⊤ = a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = arw [ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = abihimp: {α : Type ?u.37297} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(⊤ ⇨ a) ⊓ (a ⇨ ⊤) = a ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = ahimp_top: ∀ {α : Type ?u.37298} [inst : GeneralizedHeytingAlgebra α] {a : α}, a ⇨ ⊤ = ⊤
himp_top,ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(⊤ ⇨ a) ⊓ ⊤ = a ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = atop_himp: ∀ {α : Type ?u.37344} [inst : GeneralizedHeytingAlgebra α] {a : α}, ⊤ ⇨ a = a
top_himp,ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⊓ ⊤ = a ι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = ainf_top_eq: ∀ {α : Type ?u.37368} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = a
inf_top_eqι: Type ?u.37057

α: Type u_1

β: Type ?u.37063

π: ι → Type ?u.37068

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a = a]
Goals accomplished! 🐙
#align bihimp_top bihimp_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = a
bihimp_top

@[simp]
theorem top_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), ⊤ ⇔ a = a
top_bihimp : ⊤: ?m.37665
⊤ ⇔ a: α
a = a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.37634

α: Type u_1

β: Type ?u.37640

π: ι → Type ?u.37645

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

⊤ ⇔ a = arw [ι: Type ?u.37634

α: Type u_1

β: Type ?u.37640

π: ι → Type ?u.37645

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

⊤ ⇔ a = abihimp_comm: ∀ {α : Type ?u.37769} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = b ⇔ a
bihimp_comm,ι: Type ?u.37634

α: Type u_1

β: Type ?u.37640

π: ι → Type ?u.37645

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ ⊤ = a ι: Type ?u.37634

α: Type u_1

β: Type ?u.37640

π: ι → Type ?u.37645

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

⊤ ⇔ a = abihimp_top: ∀ {α : Type ?u.37803} [inst : GeneralizedHeytingAlgebra α] (a : α), a ⇔ ⊤ = a
bihimp_topι: Type ?u.37634

α: Type u_1

β: Type ?u.37640

π: ι → Type ?u.37645

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a = a]
Goals accomplished! 🐙
#align top_bihimp top_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a : α), ⊤ ⇔ a = a
top_bihimp

@[simp]
theorem bihimp_eq_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇔ b = ⊤ ↔ a = b
bihimp_eq_top {a: α
a b: α
b : α: Type ?u.37860
α} : a: α
a ⇔ b: α
b = ⊤: ?m.37946
⊤ ↔ a: α
a = b: α
b :=
  @symmDiff_eq_bot: ∀ {α : Type ?u.37999} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ∆ b = ⊥ ↔ a = b
symmDiff_eq_bot α: Type ?u.37860
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align bihimp_eq_top bihimp_eq_top: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇔ b = ⊤ ↔ a = b
bihimp_eq_top

theorem bihimp_of_le: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b → a ⇔ b = b ⇨ a
bihimp_of_le {a: α
a b: α
b : α: Type ?u.38070
α} (h: a ≤ b
h : a: α
a ≤ b: α
b) : a: α
a ⇔ b: α
b = b: α
b ⇨ a: α
a := by
Goals accomplished! 🐙
  ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ⇔ b = b ⇨ arw [ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ⇔ b = b ⇨ abihimp: {α : Type ?u.38334} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

(b ⇨ a) ⊓ (a ⇨ b) = b ⇨ a ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ⇔ b = b ⇨ ahimp_eq_top_iff: ∀ {α : Type ?u.38335} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ b
himp_eq_top_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: a ≤ b
h,ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

(b ⇨ a) ⊓ ⊤ = b ⇨ a ι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

a ⇔ b = b ⇨ ainf_top_eq: ∀ {α : Type ?u.38383} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, a ⊓ ⊤ = a
inf_top_eqι: Type ?u.38067

α: Type u_1

β: Type ?u.38073

π: ι → Type ?u.38078

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: a ≤ b

b ⇨ a = b ⇨ a]
Goals accomplished! 🐙
#align bihimp_of_le bihimp_of_le: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b → a ⇔ b = b ⇨ a
bihimp_of_le

theorem bihimp_of_ge: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ≤ a → a ⇔ b = a ⇨ b
bihimp_of_ge {a: α
a b: α
b : α: Type ?u.38630
α} (h: b ≤ a
h : b: α
b ≤ a: α
a) : a: α
a ⇔ b: α
b = a: α
a ⇨ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ⇔ b = a ⇨ brw [ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ⇔ b = a ⇨ bbihimp: {α : Type ?u.38894} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

(b ⇨ a) ⊓ (a ⇨ b) = a ⇨ b ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ⇔ b = a ⇨ bhimp_eq_top_iff: ∀ {α : Type ?u.38895} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⇨ b = ⊤ ↔ a ≤ b
himp_eq_top_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 h: b ≤ a
h,ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

⊤ ⊓ (a ⇨ b) = a ⇨ b ι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ⇔ b = a ⇨ btop_inf_eq: ∀ {α : Type ?u.38943} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {a : α}, ⊤ ⊓ a = a
top_inf_eqι: Type ?u.38627

α: Type u_1

β: Type ?u.38633

π: ι → Type ?u.38638

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: b ≤ a

a ⇨ b = a ⇨ b]
Goals accomplished! 🐙
#align bihimp_of_ge bihimp_of_ge: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, b ≤ a → a ⇔ b = a ⇨ b
bihimp_of_ge

theorem le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ⊓ b ≤ c → a ⊓ c ≤ b → a ≤ b ⇔ c
le_bihimp {a: α
a b: α
b c: α
c : α: Type ?u.39190
α} (hb: a ⊓ b ≤ c
hb : a: α
a ⊓ b: α
b ≤ c: α
c) (hc: a ⊓ c ≤ b
hc : a: α
a ⊓ c: α
c ≤ b: α
b) : a: α
a ≤ b: α
b ⇔ c: α
c :=
  le_inf: ∀ {α : Type ?u.39353} [inst : SemilatticeInf α] {a b c : α}, a ≤ b → a ≤ c → a ≤ b ⊓ c
le_inf (le_himp_iff: ∀ {α : Type ?u.39427} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ c
le_himp_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hc: a ⊓ c ≤ b
hc) <| le_himp_iff: ∀ {α : Type ?u.39457} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ c
le_himp_iff.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 hb: a ⊓ b ≤ c
hb
#align le_bihimp le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ⊓ b ≤ c → a ⊓ c ≤ b → a ≤ b ⇔ c
le_bihimp

theorem le_bihimp_iff: ∀ {a b c : α}, a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
le_bihimp_iff {a: α
a b: α
b c: α
c : α: Type ?u.39496
α} : a: α
a ≤ b: α
b ⇔ c: α
c ↔ a: α
a ⊓ b: α
b ≤ c: α
c ∧ a: α
a ⊓ c: α
c ≤ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ bsimp_rw [ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ bbihimp: {α : Type ?u.39757} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ (c ⇨ b) ⊓ (b ⇨ c) ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_inf_iff: ∀ {α : Type ?u.39854} [inst : SemilatticeInf α] {a b c : α}, a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
le_inf_iff,ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ c ⇨ b ∧ a ≤ b ⇨ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ ble_himp_iff: ∀ {α : Type ?u.40040} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇨ c ↔ a ⊓ b ≤ c
le_himp_iff,ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ⊓ c ≤ b ∧ a ⊓ b ≤ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b ι: Type ?u.39493

α: Type u_1

β: Type ?u.39499

π: ι → Type ?u.39504

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c✝, d, a, b, c: α

a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ band_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
and_comm
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align le_bihimp_iff le_bihimp_iff: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
le_bihimp_iff

@[simp]
theorem inf_le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ b ≤ a ⇔ b
inf_le_bihimp {a: α
a b: α
b : α: Type ?u.40298
α} : a: α
a ⊓ b: α
b ≤ a: α
a ⇔ b: α
b :=
  inf_le_inf: ∀ {α : Type ?u.40440} [inst : SemilatticeInf α] {a b c d : α}, a ≤ b → c ≤ d → a ⊓ c ≤ b ⊓ d
inf_le_inf le_himp: ∀ {α : Type ?u.40515} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ a
le_himp le_himp: ∀ {α : Type ?u.40540} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ≤ b ⇨ a
le_himp
#align inf_le_bihimp inf_le_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, a ⊓ b ≤ a ⇔ b
inf_le_bihimp

theorem bihimp_eq_inf_himp_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = a ⊔ b ⇨ a ⊓ b
bihimp_eq_inf_himp_inf : a: α
a ⇔ b: α
b = a: α
a ⊔ b: α
b ⇨ a: α
a ⊓ b: α
b := by
Goals accomplished! 🐙 ι: Type ?u.40596

α: Type u_1

β: Type ?u.40602

π: ι → Type ?u.40607

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇔ b = a ⊔ b ⇨ a ⊓ bsimp [himp_inf_distrib: ∀ {α : Type ?u.40752} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
himp_inf_distrib, bihimp: {α : Type ?u.40772} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp]
Goals accomplished! 🐙
#align bihimp_eq_inf_himp_inf bihimp_eq_inf_himp_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b = a ⊔ b ⇨ a ⊓ b
bihimp_eq_inf_himp_inf

theorem Codisjoint.bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇔ b = a ⊓ b
Codisjoint.bihimp_eq_inf {a: α
a b: α
b : α: Type ?u.44595
α} (h: Codisjoint a b
h : Codisjoint: {α : Type ?u.44621} → [inst : PartialOrder α] → [inst : OrderTop α] → α → α → Prop
Codisjoint a: α
a b: α
b) : a: α
a ⇔ b: α
b = a: α
a ⊓ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

a ⇔ b = a ⊓ brw [ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

a ⇔ b = a ⊓ bbihimp: {α : Type ?u.44989} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

(b ⇨ a) ⊓ (a ⇨ b) = a ⊓ b ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

a ⇔ b = a ⊓ bh: Codisjoint a b
h.himp_eq_left: ∀ {α : Type ?u.44990} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇨ b = b
himp_eq_left,ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

(b ⇨ a) ⊓ b = a ⊓ b ι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

a ⇔ b = a ⊓ bh: Codisjoint a b
h.himp_eq_right: ∀ {α : Type ?u.45022} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → b ⇨ a = a
himp_eq_rightι: Type ?u.44592

α: Type u_1

β: Type ?u.44598

π: ι → Type ?u.44603

inst✝: GeneralizedHeytingAlgebra α

a✝, b✝, c, d, a, b: α

h: Codisjoint a b

a ⊓ b = a ⊓ b]
Goals accomplished! 🐙
#align codisjoint.bihimp_eq_inf Codisjoint.bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] {a b : α}, Codisjoint a b → a ⇔ b = a ⊓ b
Codisjoint.bihimp_eq_inf

theorem himp_bihimp: a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
himp_bihimp : a: α
a ⇨ b: α
b ⇔ c: α
c = (a: α
a ⊓ c: α
c ⇨ b: α
b) ⊓ (a: α
a ⊓ b: α
b ⇨ c: α
c) := by
Goals accomplished! 🐙
  ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)rw [ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)bihimp: {α : Type ?u.45347} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp,ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ (c ⇨ b) ⊓ (b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_inf_distrib: ∀ {α : Type ?u.45348} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c)
himp_inf_distrib,ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(a ⇨ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_himp: ∀ {α : Type ?u.45387} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ c
himp_himp,ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(a ⊓ c ⇨ b) ⊓ (a ⇨ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) ι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)himp_himp: ∀ {α : Type ?u.45416} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇨ c = a ⊓ b ⇨ c
himp_himpι: Type ?u.45050

α: Type u_1

β: Type ?u.45056

π: ι → Type ?u.45061

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

(a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)]
Goals accomplished! 🐙
#align himp_bihimp himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
himp_bihimp

@[simp]
theorem sup_himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ a ⇔ b = a ⇔ b
sup_himp_bihimp : a: α
a ⊔ b: α
b ⇨ a: α
a ⇔ b: α
b = a: α
a ⇔ b: α
b := by
Goals accomplished! 🐙
  ι: Type ?u.45477

α: Type u_1

β: Type ?u.45483

π: ι → Type ?u.45488

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⊔ b ⇨ a ⇔ b = a ⇔ brw [ι: Type ?u.45477

α: Type u_1

β: Type ?u.45483

π: ι → Type ?u.45488

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⊔ b ⇨ a ⇔ b = a ⇔ bhimp_bihimp: ∀ {α : Type ?u.45646} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
himp_bihimpι: Type ?u.45477

α: Type u_1

β: Type ?u.45483

π: ι → Type ?u.45488

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b]ι: Type ?u.45477

α: Type u_1

β: Type ?u.45483

π: ι → Type ?u.45488

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
  ι: Type ?u.45477

α: Type u_1

β: Type ?u.45483

π: ι → Type ?u.45488

inst✝: GeneralizedHeytingAlgebra α

a, b, c, d: α

a ⊔ b ⇨ a ⇔ b = a ⇔ bsimp [bihimp: {α : Type ?u.45706} → [inst : Inf α] → [inst : HImp α] → α → α → α
bihimp]
Goals accomplished! 🐙
#align sup_himp_bihimp sup_himp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⊔ b ⇨ a ⇔ b = a ⇔ b
sup_himp_bihimp

@[simp]
theorem bihimp_himp_eq_inf: a ⇔ (a ⇨ b) = a ⊓ b
bihimp_himp_eq_inf : a: α
a ⇔ (a: α
a ⇨ b: α
b) = a: α
a ⊓ b: α
b :=
  @symmDiff_sdiff_eq_sup: ∀ {α : Type ?u.51996} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ (b \ a) = a ⊔ b
symmDiff_sdiff_eq_sup α: Type ?u.51895
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align bihimp_himp_eq_inf bihimp_himp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ (a ⇨ b) = a ⊓ b
bihimp_himp_eq_inf

@[simp]
theorem himp_bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (b ⇨ a) ⇔ b = a ⊓ b
himp_bihimp_eq_inf : (b: α
b ⇨ a: α
a) ⇔ b: α
b = a: α
a ⊓ b: α
b :=
  @sdiff_symmDiff_eq_sup: ∀ {α : Type ?u.52159} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a \ b) ∆ b = a ⊔ b
sdiff_symmDiff_eq_sup α: Type ?u.52058
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align himp_bihimp_eq_inf himp_bihimp_eq_inf: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (b ⇨ a) ⇔ b = a ⊓ b
himp_bihimp_eq_inf

@[simp]
theorem bihimp_inf_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⊓ (a ⊔ b) = a ⊓ b
bihimp_inf_sup : a: α
a ⇔ b: α
b ⊓ (a: α
a ⊔ b: α
b) = a: α
a ⊓ b: α
b :=
  @symmDiff_sup_inf: ∀ {α : Type ?u.52385} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ⊔ a ⊓ b = a ⊔ b
symmDiff_sup_inf α: Type ?u.52221
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align bihimp_inf_sup bihimp_inf_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⊓ (a ⊔ b) = a ⊓ b
bihimp_inf_sup

@[simp]
theorem sup_inf_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⊓ a ⇔ b = a ⊓ b
sup_inf_bihimp : (a: α
a ⊔ b: α
b) ⊓ a: α
a ⇔ b: α
b = a: α
a ⊓ b: α
b :=
  @inf_sup_symmDiff: ∀ {α : Type ?u.52615} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ⊓ b ⊔ a ∆ b = a ⊔ b
inf_sup_symmDiff α: Type ?u.52451
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align sup_inf_bihimp sup_inf_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⊓ a ⇔ b = a ⊓ b
sup_inf_bihimp

@[simp]
theorem bihimp_bihimp_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⇔ (a ⊔ b) = a ⊓ b
bihimp_bihimp_sup : a: α
a ⇔ b: α
b ⇔ (a: α
a ⊔ b: α
b) = a: α
a ⊓ b: α
b :=
  @symmDiff_symmDiff_inf: ∀ {α : Type ?u.52848} [inst : GeneralizedCoheytingAlgebra α] (a b : α), a ∆ b ∆ (a ⊓ b) = a ⊔ b
symmDiff_symmDiff_inf α: Type ?u.52683
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align bihimp_bihimp_sup bihimp_bihimp_sup: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), a ⇔ b ⇔ (a ⊔ b) = a ⊓ b
bihimp_bihimp_sup

@[simp]
theorem sup_bihimp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b
sup_bihimp_bihimp : (a: α
a ⊔ b: α
b) ⇔ (a: α
a ⇔ b: α
b) = a: α
a ⊓ b: α
b :=
  @inf_symmDiff_symmDiff: ∀ {α : Type ?u.53081} [inst : GeneralizedCoheytingAlgebra α] (a b : α), (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
inf_symmDiff_symmDiff α: Type ?u.52916
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_
#align sup_bihimp_bihimp sup_bihimp_bihimp: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⊔ b) ⇔ (a ⇔ b) = a ⊓ b
sup_bihimp_bihimp

theorem bihimp_triangle: a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c
bihimp_triangle : a: α
a ⇔ b: α
b ⊓ b: α
b ⇔ c: α
c ≤ a: α
a ⇔ c: α
c :=
  @symmDiff_triangle: ∀ {α : Type ?u.53339} [inst : GeneralizedCoheytingAlgebra α] (a b c : α), a ∆ c ≤ a ∆ b ⊔ b ∆ c
symmDiff_triangle α: Type ?u.53147
αᵒᵈ _ _: αᵒᵈ
_ _: αᵒᵈ
_ _: αᵒᵈ
_
#align bihimp_triangle bihimp_triangle: ∀ {α : Type u_1} [inst : GeneralizedHeytingAlgebra α] (a b c : α), a ⇔ b ⊓ b ⇔ c ≤ a ⇔ c
bihimp_triangle

end GeneralizedHeytingAlgebra

section CoheytingAlgebra

variable [CoheytingAlgebra: Type ?u.54510 → Type ?u.54510
CoheytingAlgebra α: Type ?u.53410
α] (a: α
a : α: Type ?u.53391
α)

@[simp]
theorem symmDiff_top': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ∆ ⊤ = ￢a
symmDiff_top' : a: α
a ∆ ⊤: ?m.53432
⊤ = ￢a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.53407

α: Type u_1

β: Type ?u.53413

π: ι → Type ?u.53418

inst✝: CoheytingAlgebra α

a: α

a ∆ ⊤ = ￢asimp [symmDiff: {α : Type ?u.53537} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff]
Goals accomplished! 🐙
#align symm_diff_top' symmDiff_top': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), a ∆ ⊤ = ￢a
symmDiff_top'

@[simp]
theorem top_symmDiff': ⊤ ∆ a = ￢a
top_symmDiff' : ⊤: ?m.54521
⊤ ∆ a: α
a = ￢a: α
a := by
Goals accomplished! 🐙 ι: Type ?u.54496

α: Type u_1

β: Type ?u.54502

π: ι → Type ?u.54507

inst✝: CoheytingAlgebra α

a: α

⊤ ∆ a = ￢asimp [symmDiff: {α : Type ?u.54638} → [inst : Sup α] → [inst : SDiff α] → α → α → α
symmDiff]
Goals accomplished! 🐙
#align top_symm_diff' top_symmDiff': ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), ⊤ ∆ a = ￢a
top_symmDiff'

@[simp]
theorem hnot_symmDiff_self: (￢a) ∆ a = ⊤
hnot_symmDiff_self : (￢a: <