text:
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import order.prop_instances

/-!
# Heyting algebras

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

This file defines Heyting, co-Heyting and bi-Heyting algebras.

An Heyting algebra is a bounded distributive lattice with an implication operation `⇨` such that
`a ≤ b ⇨ c ↔ a ⊓ b ≤ c`. It also comes with a pseudo-complement `ᶜ`, such that `aᶜ = a ⇨ ⊥`.

Co-Heyting algebras are dual to Heyting algebras. They have a difference `\` and a negation `￢`
such that `a \ b ≤ c ↔ a ≤ b ⊔ c` and `￢a = ⊤ \ a`.

Bi-Heyting algebras are Heyting algebras that are also co-Heyting algebras.

From a logic standpoint, Heyting algebras precisely model intuitionistic logic, whereas boolean
algebras model classical logic.

Heyting algebras are the order theoretic equivalent of cartesian-closed categories.

## Main declarations

* `generalized_heyting_algebra`: Heyting algebra without a top element (nor negation).
* `generalized_coheyting_algebra`: Co-Heyting algebra without a bottom element (nor complement).
* `heyting_algebra`: Heyting algebra.
* `coheyting_algebra`: Co-Heyting algebra.
* `biheyting_algebra`: bi-Heyting algebra.

## Notation

* `⇨`: Heyting implication
* `\`: Difference
* `￢`: Heyting negation
* `ᶜ`: (Pseudo-)complement

## References

* [Francis Borceux, *Handbook of Categorical Algebra III*][borceux-vol3]

## Tags

Heyting, Brouwer, algebra, implication, negation, intuitionistic
-/

set_option old_structure_cmd true

open function order_dual

universes u
variables {ι α β : Type*}

/-! ### Notation -/

/-- Syntax typeclass for Heyting implication `⇨`. -/
@[notation_class] class has_himp (α : Type*) := (himp : α → α → α)

/-- Syntax typeclass for Heyting negation `￢`.

The difference between `has_compl` and `has_hnot` is that the former belongs to Heyting algebras,
while the latter belongs to co-Heyting algebras. They are both pseudo-complements, but `compl`
underestimates while `hnot` overestimates. In boolean algebras, they are equal. See `hnot_eq_compl`.
-/
@[notation_class] class has_hnot (α : Type*) := (hnot : α → α)

export has_himp (himp) has_sdiff (sdiff) has_hnot (hnot)

infixr ` ⇨ `:60 := himp
prefix `￢`:72 := hnot

instance [has_himp α] [has_himp β] : has_himp (α × β) := ⟨λ a b, (a.1 ⇨ b.1, a.2 ⇨ b.2)⟩
instance [has_hnot α] [has_hnot β] : has_hnot (α × β) := ⟨λ a, (￢a.1, ￢a.2)⟩
instance [has_sdiff α] [has_sdiff β] : has_sdiff (α × β) := ⟨λ a b, (a.1 \ b.1, a.2 \ b.2)⟩
instance [has_compl α] [has_compl β] : has_compl (α × β) := ⟨λ a, (a.1ᶜ, a.2ᶜ)⟩

@[simp] lemma fst_himp [has_himp α] [has_himp β] (a b : α × β) : (a ⇨ b).1 = a.1 ⇨ b.1 := rfl
@[simp] lemma snd_himp [has_himp α] [has_himp β] (a b : α × β) : (a ⇨ b).2 = a.2 ⇨ b.2 := rfl
@[simp] lemma fst_hnot [has_hnot α] [has_hnot β] (a : α × β) : (￢a).1 = ￢a.1 := rfl
@[simp] lemma snd_hnot [has_hnot α] [has_hnot β] (a : α × β) : (￢a).2 = ￢a.2 := rfl
@[simp] lemma fst_sdiff [has_sdiff α] [has_sdiff β] (a b : α × β) : (a \ b).1 = a.1 \ b.1 := rfl
@[simp] lemma snd_sdiff [has_sdiff α] [has_sdiff β] (a b : α × β) : (a \ b).2 = a.2 \ b.2 := rfl
@[simp] lemma fst_compl [has_compl α] [has_compl β] (a : α × β) : aᶜ.1 = a.1ᶜ := rfl
@[simp] lemma snd_compl [has_compl α] [has_compl β] (a : α × β) : aᶜ.2 = a.2ᶜ := rfl

namespace pi
variables {π : ι → Type*}

instance [Π i, has_himp (π i)] : has_himp (Π i, π i) := ⟨λ a b i, a i ⇨ b i⟩
instance [Π i, has_hnot (π i)] : has_hnot (Π i, π i) := ⟨λ a i, ￢a i⟩

lemma himp_def [Π i, has_himp (π i)] (a b : Π i, π i) : (a ⇨ b) = λ i, a i ⇨ b i := rfl
lemma hnot_def [Π i, has_hnot (π i)] (a : Π i, π i) : ￢a = λ i, ￢a i := rfl

@[simp] lemma himp_apply [Π i, has_himp (π i)] (a b : Π i, π i) (i : ι) : (a ⇨ b) i = a i ⇨ b i :=
rfl
@[simp] lemma hnot_apply [Π i, has_hnot (π i)] (a : Π i, π i) (i : ι) : (￢a) i = ￢a i := rfl

end pi

/-- A generalized Heyting algebra is a lattice with an additional binary operation `⇨` called
Heyting implication such that `a ⇨` is right adjoint to `a ⊓`.

 This generalizes `heyting_algebra` by not requiring a bottom element. -/
class generalized_heyting_algebra (α : Type*) extends lattice α, has_top α, has_himp α :=
(le_top : ∀ a : α, a ≤ ⊤)
(le_himp_iff (a b c : α) : a ≤ b ⇨ c ↔ a ⊓ b ≤ c)

/-- A generalized co-Heyting algebra is a lattice with an additional binary difference operation `\`
such that `\ a` is right adjoint to `⊔ a`.

This generalizes `coheyting_algebra` by not requiring a top element. -/
class generalized_coheyting_algebra (α : Type*) extends lattice α, has_bot α, has_sdiff α :=
(bot_le : ∀ a : α, ⊥ ≤ a)
(sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c)

/-- A Heyting algebra is a bounded lattice with an additional binary operation `⇨` called Heyting
implication such that `a ⇨` is right adjoint to `a ⊓`. -/
class heyting_algebra (α : Type*) extends generalized_heyting_algebra α, has_bot α, has_compl α :=
(bot_le : ∀ a : α, ⊥ ≤ a)
(himp_bot (a : α) : a ⇨ ⊥ = aᶜ)

/-- A co-Heyting algebra is a bounded  lattice with an additional binary difference operation `\`
such that `\ a` is right adjoint to `⊔ a`. -/
class coheyting_algebra (α : Type*)
  extends generalized_coheyting_algebra α, has_top α, has_hnot α :=
(le_top : ∀ a : α, a ≤ ⊤)
(top_sdiff (a : α) : ⊤ \ a = ￢a)

/-- A bi-Heyting algebra is a Heyting algebra that is also a co-Heyting algebra. -/
class biheyting_algebra (α : Type*) extends heyting_algebra α, has_sdiff α, has_hnot α :=
(sdiff_le_iff (a b c : α) : a \ b ≤ c ↔ a ≤ b ⊔ c)
(top_sdiff (a : α) : ⊤ \ a = ￢a)

@[priority 100] -- See note [lower instance priority]
instance generalized_heyting_algebra.to_order_top [generalized_heyting_algebra α] : order_top α :=
{ ..‹generalized_heyting_algebra α› }

@[priority 100] -- See note [lower instance priority]
instance generalized_coheyting_algebra.to_order_bot [generalized_coheyting_algebra α] :
  order_bot α :=
{ ..‹generalized_coheyting_algebra α› }

@[priority 100] -- See note [lower instance priority]
instance heyting_algebra.to_bounded_order [heyting_algebra α] : bounded_order α :=
{ ..‹heyting_algebra α› }

@[priority 100] -- See note [lower instance priority]
instance coheyting_algebra.to_bounded_order [coheyting_algebra α] : bounded_order α :=
{ ..‹coheyting_algebra α› }

@[priority 100] -- See note [lower instance priority]
instance biheyting_algebra.to_coheyting_algebra [biheyting_algebra α] : coheyting_algebra α :=
{ ..‹biheyting_algebra α› }

/-- Construct a Heyting algebra from the lattice structure and Heyting implication alone. -/
@[reducible] -- See note [reducible non-instances]
def heyting_algebra.of_himp [distrib_lattice α] [bounded_order α] (himp : α → α → α)
  (le_himp_iff : ∀ a b c, a ≤ himp b c ↔ a ⊓ b ≤ c) : heyting_algebra α :=
{ himp := himp,
  compl := λ a, himp a ⊥,
  le_himp_iff := le_himp_iff,
  himp_bot := λ a, rfl,
  ..‹distrib_lattice α›, ..‹bounded_order α› }

/-- Construct a Heyting algebra from the lattice structure and complement operator alone. -/
@[reducible] -- See note [reducible non-instances]
def heyting_algebra.of_compl [distrib_lattice α] [bounded_order α] (compl : α → α)
  (le_himp_iff : ∀ a b c, a ≤ compl b ⊔ c ↔ a ⊓ b ≤ c) : heyting_algebra α :=
{ himp := λ a, (⊔) (compl a),
  compl := compl,
  le_himp_iff := le_himp_iff,
  himp_bot := λ a, sup_bot_eq,
  ..‹distrib_lattice α›, ..‹bounded_order α› }

/-- Construct a co-Heyting algebra from the lattice structure and the difference alone. -/
@[reducible] -- See note [reducible non-instances]
def coheyting_algebra.of_sdiff [distrib_lattice α] [bounded_order α] (sdiff : α → α → α)
  (sdiff_le_iff : ∀ a b c, sdiff a b ≤ c ↔ a ≤ b ⊔ c) : coheyting_algebra α :=
{ sdiff := sdiff,
  hnot := λ a, sdiff ⊤ a,
  sdiff_le_iff := sdiff_le_iff,
  top_sdiff := λ a, rfl,
  ..‹distrib_lattice α›, ..‹bounded_order α› }

/-- Construct a co-Heyting algebra from the difference and Heyting negation alone. -/
@[reducible] -- See note [reducible non-instances]
def coheyting_algebra.of_hnot [distrib_lattice α] [bounded_order α] (hnot : α → α)
  (sdiff_le_iff : ∀ a b c, a ⊓ hnot b ≤ c ↔ a ≤ b ⊔ c) : coheyting_algebra α :=
{ sdiff := λ a b, (a ⊓ hnot b),
  hnot := hnot,
  sdiff_le_iff := sdiff_le_iff,
  top_sdiff := λ a, top_inf_eq,
  ..‹distrib_lattice α›, ..‹bounded_order α› }

section generalized_heyting_algebra
variables [generalized_heyting_algebra α] {a b c d : α}

/- In this section, we'll give interpretations of these results in the Heyting algebra model of
intuitionistic logic,- where `≤` can be interpreted as "validates", `⇨` as "implies", `⊓` as "and",
`⊔` as "or", `⊥` as "false" and `⊤` as "true". Note that we confuse `→` and `⊢` because those are
the same in this logic.

See also `Prop.heyting_algebra`. -/

-- `p → q → r ↔ p ∧ q → r`
@[simp] lemma le_himp_iff : a ≤ b ⇨ c ↔ a ⊓ b ≤ c := generalized_heyting_algebra.le_himp_iff _ _ _

-- `p → q → r ↔ q ∧ p → r`
lemma le_himp_iff' : a ≤ b ⇨ c ↔ b ⊓ a ≤ c := by rw [le_himp_iff, inf_comm]

-- `p → q → r ↔ q → p → r`
lemma le_himp_comm : a ≤ b ⇨ c ↔ b ≤ a ⇨ c := by rw [le_himp_iff, le_himp_iff']

-- `p → q → p`
lemma le_himp : a ≤ b ⇨ a := le_himp_iff.2 inf_le_left

-- `p → p → q ↔ p → q`
@[simp] lemma le_himp_iff_left : a ≤ a ⇨ b ↔ a ≤ b := by rw [le_himp_iff, inf_idem]

-- `p → p`
@[simp] lemma himp_self : a ⇨ a = ⊤ := top_le_iff.1 $ le_himp_iff.2 inf_le_right

-- `(p → q) ∧ p → q`
lemma himp_inf_le : (a ⇨ b) ⊓ a ≤ b := le_himp_iff.1 le_rfl

-- `p ∧ (p → q) → q`
lemma inf_himp_le : a ⊓ (a ⇨ b) ≤ b := by rw [inf_comm, ←le_himp_iff]

-- `p ∧ (p → q) ↔ p ∧ q`
@[simp] lemma inf_himp (a b : α) : a ⊓ (a ⇨ b) = a ⊓ b :=
le_antisymm (le_inf inf_le_left $ by rw [inf_comm, ←le_himp_iff]) $ inf_le_inf_left _ le_himp

-- `(p → q) ∧ p ↔ q ∧ p`
@[simp] lemma himp_inf_self (a b : α) : (a ⇨ b) ⊓ a = b ⊓ a := by rw [inf_comm, inf_himp, inf_comm]

/-- The **deduction theorem** in the Heyting algebra model of intuitionistic logic:
an implication holds iff the conclusion follows from the hypothesis. -/
@[simp] lemma himp_eq_top_iff : a ⇨ b = ⊤ ↔ a ≤ b := by rw [←top_le_iff, le_himp_iff, top_inf_eq]

-- `p → true`, `true → p ↔ p`
@[simp] lemma himp_top : a ⇨ ⊤ = ⊤ := himp_eq_top_iff.2 le_top
@[simp] lemma top_himp : ⊤ ⇨ a = a := eq_of_forall_le_iff $ λ b, by rw [le_himp_iff, inf_top_eq]

-- `p → q → r ↔ p ∧ q → r`
lemma himp_himp (a b c : α) : a ⇨ b ⇨ c = a ⊓ b ⇨ c :=
eq_of_forall_le_iff $ λ d, by simp_rw [le_himp_iff, inf_assoc]

-- `(q → r) → (p → q) → q → r`
@[simp] lemma himp_le_himp_himp_himp : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c :=
begin
  rw [le_himp_iff, le_himp_iff, inf_assoc, himp_inf_self, ←inf_assoc, himp_inf_self, inf_assoc],
  exact inf_le_left,
end

-- `p → q → r ↔ q → p → r`
lemma himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c := by simp_rw [himp_himp, inf_comm]

@[simp] lemma himp_idem : b ⇨ b ⇨ a = b ⇨ a := by rw [himp_himp, inf_idem]

lemma himp_inf_distrib (a b c : α) : a ⇨ b ⊓ c = (a ⇨ b) ⊓ (a ⇨ c) :=
eq_of_forall_le_iff $ λ d, by simp_rw [le_himp_iff, le_inf_iff, le_himp_iff]

lemma sup_himp_distrib (a b c : α) : a ⊔ b ⇨ c = (a ⇨ c) ⊓ (b ⇨ c) :=
eq_of_forall_le_iff $ λ d, by { rw [le_inf_iff, le_himp_comm, sup_le_iff], simp_rw le_himp_comm }

lemma himp_le_himp_left (h : a ≤ b) : c ⇨ a ≤ c ⇨ b := le_himp_iff.2 $ himp_inf_le.trans h

lemma himp_le_himp_right (h : a ≤ b) : b ⇨ c ≤ a ⇨ c :=
le_himp_iff.2 $ (inf_le_inf_left _ h).trans himp_inf_le

lemma himp_le_himp (hab : a ≤ b) (hcd : c ≤ d) : b ⇨ c ≤ a ⇨ d :=
(himp_le_himp_right hab).trans $ himp_le_himp_left hcd

@[simp] lemma sup_himp_self_left (a b : α) : (a ⊔ b) ⇨ a = b ⇨ a :=
by rw [sup_himp_distrib, himp_self, top_inf_eq]

@[simp] lemma sup_himp_self_right (a b : α) : (a ⊔ b) ⇨ b = a ⇨ b :=
by rw [sup_himp_distrib, himp_self, inf_top_eq]

lemma codisjoint.himp_eq_right (h : codisjoint a b) : b ⇨ a = a :=
by { conv_rhs { rw ←@top_himp _ _ a }, rw [←h.eq_top, sup_himp_self_left] }

lemma codisjoint.himp_eq_left (h : codisjoint a b) : a ⇨ b = b := h.symm.himp_eq_right

lemma codisjoint.himp_inf_cancel_right (h : codisjoint a b) : a ⇨ (a ⊓ b) = b :=
by rw [himp_inf_distrib, himp_self, top_inf_eq, h.himp_eq_left]

lemma codisjoint.himp_inf_cancel_left (h : codisjoint a b) : b ⇨ (a ⊓ b) = a :=
by rw [himp_inf_distrib, himp_self, inf_top_eq, h.himp_eq_right]

lemma le_himp_himp : a ≤ (a ⇨ b) ⇨ b := le_himp_iff.2 inf_himp_le

lemma himp_triangle (a b c : α) : (a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c :=
by { rw [le_himp_iff, inf_right_comm, ←le_himp_iff], exact himp_inf_le.trans le_himp_himp }

lemma himp_inf_himp_cancel (hba : b ≤ a) (hcb : c ≤ b) : (a ⇨ b) ⊓ (b ⇨ c) = a ⇨ c :=
(himp_triangle  _ _ _).antisymm $ le_inf (himp_le_himp_left hcb) (himp_le_himp_right hba)

@[priority 100] -- See note [lower instance priority]
instance generalized_heyting_algebra.to_distrib_lattice : distrib_lattice α :=
distrib_lattice.of_inf_sup_le $ λ a b c,
  by simp_rw [@inf_comm _ _ a, ←le_himp_iff, sup_le_iff, le_himp_iff, ←sup_le_iff]

instance : generalized_coheyting_algebra αᵒᵈ :=
{ sdiff := λ a b, to_dual (of_dual b ⇨ of_dual a),
  sdiff_le_iff := λ a b c, by { rw sup_comm, exact le_himp_iff },
  ..order_dual.lattice α, ..order_dual.order_bot α }

instance prod.generalized_heyting_algebra [generalized_heyting_algebra β] :
  generalized_heyting_algebra (α × β) :=
{ le_himp_iff := λ a b c, and_congr le_himp_iff le_himp_iff,
  ..prod.lattice α β, ..prod.order_top α β, ..prod.has_himp, ..prod.has_compl }

instance pi.generalized_heyting_algebra {α : ι → Type*} [Π i, generalized_heyting_algebra (α i)] :
  generalized_heyting_algebra (Π i, α i) :=
by { pi_instance, exact λ a b c, forall_congr (λ i, le_himp_iff) }

end generalized_heyting_algebra

section generalized_coheyting_algebra
variables [generalized_coheyting_algebra α] {a b c d : α}

@[simp] lemma sdiff_le_iff : a \ b ≤ c ↔ a ≤ b ⊔ c :=
generalized_coheyting_algebra.sdiff_le_iff _ _ _

lemma sdiff_le_iff' : a \ b ≤ c ↔ a ≤ c ⊔ b := by rw [sdiff_le_iff, sup_comm]

lemma sdiff_le_comm : a \ b ≤ c ↔ a \ c ≤ b := by rw [sdiff_le_iff, sdiff_le_iff']

lemma sdiff_le : a \ b ≤ a := sdiff_le_iff.2 le_sup_right

lemma disjoint.disjoint_sdiff_left (h : disjoint a b) : disjoint (a \ c) b := h.mono_left sdiff_le
lemma disjoint.disjoint_sdiff_right (h : disjoint a b) : disjoint a (b \ c) := h.mono_right sdiff_le

@[simp] lemma sdiff_le_iff_left : a \ b ≤ b ↔ a ≤ b := by rw [sdiff_le_iff, sup_idem]

@[simp] lemma sdiff_self : a \ a = ⊥ := le_bot_iff.1 $ sdiff_le_iff.2 le_sup_left

lemma le_sup_sdiff : a ≤ b ⊔ a \ b := sdiff_le_iff.1 le_rfl
lemma le_sdiff_sup : a ≤ a \ b ⊔ b := by rw [sup_comm, ←sdiff_le_iff]

@[simp] lemma sup_sdiff_left : a ⊔ a \ b = a := sup_of_le_left sdiff_le
@[simp] lemma sup_sdiff_right : a \ b ⊔ a = a := sup_of_le_right sdiff_le
@[simp] lemma inf_sdiff_left : a \ b ⊓ a = a \ b := inf_of_le_left sdiff_le
@[simp] lemma inf_sdiff_right : a ⊓ a \ b = a \ b := inf_of_le_right sdiff_le

@[simp] lemma sup_sdiff_self (a b : α) : a ⊔ b \ a = a ⊔ b :=
le_antisymm (sup_le_sup_left sdiff_le _) (sup_le le_sup_left le_sup_sdiff)

@[simp] lemma sdiff_sup_self (a b : α) : b \ a ⊔ a = b ⊔ a :=
by rw [sup_comm, sup_sdiff_self, sup_comm]

alias sdiff_sup_self ← sup_sdiff_self_left
alias sup_sdiff_self ← sup_sdiff_self_right

lemma sup_sdiff_eq_sup (h : c ≤ a) : a ⊔ b \ c = a ⊔ b :=
sup_congr_left (sdiff_le.trans le_sup_right) $ le_sup_sdiff.trans $ sup_le_sup_right h _

-- cf. `set.union_diff_cancel'`
lemma sup_sdiff_cancel' (hab : a ≤ b) (hbc : b ≤ c) : b ⊔ c \ a = c :=
by rw [sup_sdiff_eq_sup hab, sup_of_le_right hbc]

lemma sup_sdiff_cancel_right (h : a ≤ b) : a ⊔ b \ a = b := sup_sdiff_cancel' le_rfl h

lemma sdiff_sup_cancel (h : b ≤ a) : a \ b ⊔ b = a := by rw [sup_comm, sup_sdiff_cancel_right h]

lemma sup_le_of_le_sdiff_left (h : b ≤ c \ a) (hac : a ≤ c) : a ⊔ b ≤ c :=
sup_le hac $ h.trans sdiff_le

lemma sup_le_of_le_sdiff_right (h : a ≤ c \ b) (hbc : b ≤ c) : a ⊔ b ≤ c :=
sup_le (h.trans sdiff_le) hbc

@[simp] lemma sdiff_eq_bot_iff : a \ b = ⊥ ↔ a ≤ b := by rw [←le_bot_iff, sdiff_le_iff, sup_bot_eq]

@[simp] lemma sdiff_bot : a \ ⊥ = a := eq_of_forall_ge_iff $ λ b, by rw [sdiff_le_iff, bot_sup_eq]
@[simp] lemma bot_sdiff : ⊥ \ a = ⊥ := sdiff_eq_bot_iff.2 bot_le

@[simp] lemma sdiff_sdiff_sdiff_le_sdiff : a \ b \ (a \ c) ≤ c \ b :=
begin
  rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
    sup_left_comm],
  exact le_sup_left,
end

lemma sdiff_sdiff (a b c : α) : a \ b \ c = a \ (b ⊔ c) :=
eq_of_forall_ge_iff $ λ d, by simp_rw [sdiff_le_iff, sup_assoc]

lemma sdiff_sdiff_left : a \ b \ c = a \ (b ⊔ c) := sdiff_sdiff _ _ _

lemma sdiff_right_comm (a b c : α) : a \ b \ c = a \ c \ b := by simp_rw [sdiff_sdiff, sup_comm]

lemma sdiff_sdiff_comm : a \ b \ c = a \ c \ b := sdiff_right_comm _ _ _

@[simp] lemma sdiff_idem : a \ b \ b = a \ b := by rw [sdiff_sdiff_left, sup_idem]
@[simp] lemma sdiff_sdiff_self : a \ b \ a = ⊥ := by rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

lemma sup_sdiff_distrib (a b c : α) : (a ⊔ b) \ c = a \ c ⊔ b \ c :=
eq_of_forall_ge_iff $ λ d, by simp_rw [sdiff_le_iff, sup_le_iff, sdiff_le_iff]

lemma sdiff_inf_distrib (a b c : α) : a \ (b ⊓ c) = a \ b ⊔ a \ c :=
eq_of_forall_ge_iff $ λ d, by { rw [sup_le_iff, sdiff_le_comm, le_inf_iff], simp_rw sdiff_le_comm }

lemma sup_sdiff : (a ⊔ b) \ c = a \ c ⊔ b \ c := sup_sdiff_distrib _ _ _

@[simp] lemma sup_sdiff_right_self : (a ⊔ b) \ b = a \ b :=
by rw [sup_sdiff, sdiff_self, sup_bot_eq]

@[simp] lemma sup_sdiff_left_self : (a ⊔ b) \ a = b \ a := by rw [sup_comm, sup_sdiff_right_self]

lemma sdiff_le_sdiff_right (h : a ≤ b) : a \ c ≤ b \ c := sdiff_le_iff.2 $ h.trans $ le_sup_sdiff

lemma sdiff_le_sdiff_left (h : a ≤ b) : c \ b ≤ c \ a :=
sdiff_le_iff.2 $ le_sup_sdiff.trans $ sup_le_sup_right h _

lemma sdiff_le_sdiff (hab : a ≤ b) (hcd : c ≤ d) : a \ d ≤ b \ c :=
(sdiff_le_sdiff_right hab).trans $ sdiff_le_sdiff_left hcd

-- cf. `is_compl.inf_sup`
lemma sdiff_inf : a \ (b ⊓ c) = a \ b ⊔ a \ c := sdiff_inf_distrib _ _ _

@[simp] lemma sdiff_inf_self_left (a b : α) : a \ (a ⊓ b) = a \ b :=
by rw [sdiff_inf, sdiff_self, bot_sup_eq]

@[simp] lemma sdiff_inf_self_right (a b : α) : b \ (a ⊓ b) = b \ a :=
by rw [sdiff_inf, sdiff_self, sup_bot_eq]

lemma disjoint.sdiff_eq_left (h : disjoint a b) : a \ b = a :=
by { conv_rhs { rw ←@sdiff_bot _ _ a }, rw [←h.eq_bot, sdiff_inf_self_left] }

lemma disjoint.sdiff_eq_right (h : disjoint a b) : b \ a = b := h.symm.sdiff_eq_left

lemma disjoint.sup_sdiff_cancel_left (h : disjoint a b) : (a ⊔ b) \ a = b :=
by rw [sup_sdiff, sdiff_self, bot_sup_eq, h.sdiff_eq_right]

lemma disjoint.sup_sdiff_cancel_right (h : disjoint a b) : (a ⊔ b) \ b = a :=
by rw [sup_sdiff, sdiff_self, sup_bot_eq, h.sdiff_eq_left]

lemma sdiff_sdiff_le : a \ (a \ b) ≤ b := sdiff_le_iff.2 le_sdiff_sup

lemma sdiff_triangle (a b c : α) : a \ c ≤ a \ b ⊔ b \ c :=
by { rw [sdiff_le_iff, sup_left_comm, ←sdiff_le_iff], exact sdiff_sdiff_le.trans le_sup_sdiff }

lemma sdiff_sup_sdiff_cancel (hba : b ≤ a) (hcb : c ≤ b) : a \ b ⊔ b \ c = a \ c :=
(sdiff_triangle  _ _ _).antisymm' $ sup_le (sdiff_le_sdiff_left hcb) (sdiff_le_sdiff_right hba)

lemma sdiff_le_sdiff_of_sup_le_sup_left (h : c ⊔ a ≤ c ⊔ b) : a \ c ≤ b \ c :=
by { rw [←sup_sdiff_left_self, ←@sup_sdiff_left_self _ _ _ b], exact sdiff_le_sdiff_right h }

lemma sdiff_le_sdiff_of_sup_le_sup_right (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c :=
by { rw [←sup_sdiff_right_self, ←@sup_sdiff_right_self _ _ b], exact sdiff_le_sdiff_right h }

@[simp] lemma inf_sdiff_sup_left : a \ c ⊓ (a ⊔ b) = a \ c :=
inf_of_le_left $ sdiff_le.trans le_sup_left
@[simp] lemma inf_sdiff_sup_right : a \ c ⊓ (b ⊔ a) = a \ c :=
inf_of_le_left $ sdiff_le.trans le_sup_right

@[priority 100] -- See note [lower instance priority]
instance generalized_coheyting_algebra.to_distrib_lattice : distrib_lattice α :=
{ le_sup_inf := λ a b c, by simp_rw [←sdiff_le_iff, le_inf_iff, sdiff_le_iff, ←le_inf_iff],
  ..‹generalized_coheyting_algebra α› }

instance : generalized_heyting_algebra αᵒᵈ :=
{ himp := λ a b, to_dual (of_dual b \ of_dual a),
  le_himp_iff := λ a b c, by { rw inf_comm, exact sdiff_le_iff },
  ..order_dual.lattice α, ..order_dual.order_top α }

instance prod.generalized_coheyting_algebra [generalized_coheyting_algebra β] :
  generalized_coheyting_algebra (α × β) :=
{ sdiff_le_iff := λ a b c, and_congr sdiff_le_iff sdiff_le_iff,
  ..prod.lattice α β, ..prod.order_bot α β, ..prod.has_sdiff, ..prod.has_hnot }

instance pi.generalized_coheyting_algebra {α : ι → Type*}
  [Π i, generalized_coheyting_algebra (α i)] : generalized_coheyting_algebra (Π i, α i) :=
by { pi_instance, exact λ a b c, forall_congr (λ i, sdiff_le_iff) }

end generalized_coheyting_algebra

section heyting_algebra
variables [heyting_algebra α] {a b c : α}

@[simp] lemma himp_bot (a : α) : a ⇨ ⊥ = aᶜ := heyting_algebra.himp_bot _
@[simp] lemma bot_himp (a : α) : ⊥ ⇨ a = ⊤ := himp_eq_top_iff.2 bot_le

lemma compl_sup_distrib (a b : α) : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ := by simp_rw [←himp_bot, sup_himp_distrib]
@[simp] lemma compl_sup : (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ := compl_sup_distrib _ _

lemma compl_le_himp : aᶜ ≤ a ⇨ b := (himp_bot _).ge.trans $ himp_le_himp_left bot_le

lemma compl_sup_le_himp : aᶜ ⊔ b ≤ a ⇨ b := sup_le compl_le_himp le_himp
lemma sup_compl_le_himp : b ⊔ aᶜ ≤ a ⇨ b := sup_le le_himp compl_le_himp

-- `p → ¬ p ↔ ¬ p`
@[simp] lemma himp_compl (a : α) : a ⇨ aᶜ = aᶜ := by rw [←himp_bot, himp_himp, inf_idem]

-- `p → ¬ q ↔ q → ¬ p`
lemma himp_compl_comm (a b : α) : a ⇨ bᶜ = b ⇨ aᶜ := by simp_rw [←himp_bot, himp_left_comm]

lemma le_compl_iff_disjoint_right : a ≤ bᶜ ↔ disjoint a b :=
by rw [←himp_bot, le_himp_iff, disjoint_iff_inf_le]

lemma le_compl_iff_disjoint_left : a ≤ bᶜ ↔ disjoint b a :=
le_compl_iff_disjoint_right.trans disjoint.comm

lemma le_compl_comm : a ≤ bᶜ ↔ b ≤ aᶜ :=
by rw [le_compl_iff_disjoint_right, le_compl_iff_disjoint_left]

alias le_compl_iff_disjoint_right ↔ _ disjoint.le_compl_right
alias le_compl_iff_disjoint_left ↔ _ disjoint.le_compl_left
alias le_compl_comm ← le_compl_iff_le_compl
alias le_compl_comm ↔ le_compl_of_le_compl _

lemma disjoint_compl_left : disjoint aᶜ a := disjoint_iff_inf_le.mpr $ le_himp_iff.1 (himp_bot _).ge
lemma disjoint_compl_right : disjoint a aᶜ := disjoint_compl_left.symm

lemma has_le.le.disjoint_compl_left (h : b ≤ a) : disjoint aᶜ b := disjoint_compl_left.mono_right h
lemma has_le.le.disjoint_compl_right (h : a ≤ b) : disjoint a bᶜ := disjoint_compl_right.mono_left h

lemma is_compl.compl_eq (h : is_compl a b) : aᶜ = b :=
h.1.le_compl_left.antisymm' $ disjoint.le_of_codisjoint disjoint_compl_left h.2

lemma is_compl.eq_compl (h : is_compl a b) : a = bᶜ :=
h.1.le_compl_right.antisymm $ disjoint.le_of_codisjoint disjoint_compl_left h.2.symm

lemma compl_unique (h₀ : a ⊓ b = ⊥) (h₁ : a ⊔ b = ⊤) : aᶜ = b := (is_compl.of_eq h₀ h₁).compl_eq

@[simp] lemma inf_compl_self (a : α) : a ⊓ aᶜ = ⊥ := disjoint_compl_right.eq_bot
@[simp] lemma compl_inf_self (a : α) : aᶜ ⊓ a = ⊥ := disjoint_compl_left.eq_bot
lemma inf_compl_eq_bot : a ⊓ aᶜ = ⊥ := inf_compl_self _
lemma compl_inf_eq_bot : aᶜ ⊓ a = ⊥ := compl_inf_self _

@[simp] lemma compl_top : (⊤ : α)ᶜ = ⊥ :=
eq_of_forall_le_iff $ λ a, by rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

@[simp] lemma compl_bot : (⊥ : α)ᶜ = ⊤ := by rw [←himp_bot, himp_self]

lemma le_compl_compl : a ≤ aᶜᶜ := disjoint_compl_right.le_compl_right

lemma compl_anti : antitone (compl : α → α) := λ a b h, le_compl_comm.1 $ h.trans le_compl_compl

lemma compl_le_compl (h : a ≤ b) : bᶜ ≤ aᶜ := compl_anti h

@[simp] lemma compl_compl_compl (a : α) : aᶜᶜᶜ = aᶜ :=
(compl_anti le_compl_compl).antisymm le_compl_compl

@[simp] lemma disjoint_compl_compl_left_iff : disjoint aᶜᶜ b ↔ disjoint a b :=
by simp_rw [←le_compl_iff_disjoint_left, compl_compl_compl]

@[simp] lemma disjoint_compl_compl_right_iff : disjoint a bᶜᶜ ↔ disjoint a b :=
by simp_rw [←le_compl_iff_disjoint_right, compl_compl_compl]

lemma compl_sup_compl_le :  aᶜ ⊔ bᶜ ≤ (a ⊓ b)ᶜ :=
sup_le (compl_anti inf_le_left) $ compl_anti inf_le_right

lemma compl_compl_inf_distrib (a b : α) : (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ :=
begin
  refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm _,
  rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff,
    disjoint_left_comm, disjoint_compl_compl_left_iff, ←disjoint_assoc, inf_comm],
  exact disjoint_compl_right,
end

lemma compl_compl_himp_distrib (a b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ :=
begin
  refine le_antisymm _ _,
  { rw [le_himp_iff, ←compl_compl_inf_distrib],
    exact compl_anti (compl_anti himp_inf_le) },
  { refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans _),
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm,
      ←le_compl_iff_disjoint_right],
    exact inf_himp_le }
end

instance : coheyting_algebra αᵒᵈ :=
{ hnot := to_dual ∘ compl ∘ of_dual,
  sdiff := λ a b, to_dual (of_dual b ⇨ of_dual a),
  sdiff_le_iff := λ a b c, by { rw sup_comm, exact le_himp_iff },
  top_sdiff := himp_bot,
  ..order_dual.lattice α, ..order_dual.bounded_order α }

@[simp] lemma of_dual_hnot (a : αᵒᵈ) : of_dual ￢a = (of_dual a)ᶜ := rfl
@[simp] lemma to_dual_compl (a : α) : to_dual aᶜ = ￢to_dual a := rfl

instance prod.heyting_algebra [heyting_algebra β] : heyting_algebra (α × β) :=
{ himp_bot := λ a, prod.ext (himp_bot a.1) (himp_bot a.2),
  ..prod.generalized_heyting_algebra, ..prod.bounded_order α β, ..prod.has_compl }

instance pi.heyting_algebra {α : ι → Type*} [Π i, heyting_algebra (α i)] :
  heyting_algebra (Π i, α i) :=
by { pi_instance, exact λ a b c, forall_congr (λ i, le_himp_iff) }

end heyting_algebra

section coheyting_algebra
variables [coheyting_algebra α] {a b c : α}

@[simp] lemma top_sdiff' (a : α) : ⊤ \ a = ￢a := coheyting_algebra.top_sdiff _
@[simp] lemma sdiff_top (a : α) : a \ ⊤ = ⊥ := sdiff_eq_bot_iff.2 le_top

lemma hnot_inf_distrib (a b : α) : ￢ (a ⊓ b) = ￢a ⊔ ￢b :=
by simp_rw [←top_sdiff', sdiff_inf_distrib]

lemma sdiff_le_hnot : a \ b ≤ ￢b := (sdiff_le_sdiff_right le_top).trans_eq $ top_sdiff' _

lemma sdiff_le_inf_hnot : a \ b ≤ a ⊓ ￢b := le_inf sdiff_le sdiff_le_hnot

@[priority 100] -- See note [lower instance priority]
instance coheyting_algebra.to_distrib_lattice : distrib_lattice α :=
{ le_sup_inf := λ a b c, by simp_rw [←sdiff_le_iff, le_inf_iff, sdiff_le_iff, ←le_inf_iff],
  ..‹coheyting_algebra α› }

@[simp] lemma hnot_sdiff (a : α) : ￢a \ a = ￢a := by rw [←top_sdiff', sdiff_sdiff, sup_idem]

lemma hnot_sdiff_comm (a b : α) : ￢a \ b = ￢b \ a := by simp_rw [←top_sdiff', sdiff_right_comm]

lemma hnot_le_iff_codisjoint_right : ￢a ≤ b ↔ codisjoint a b :=
by rw [←top_sdiff', sdiff_le_iff, codisjoint_iff_le_sup]

lemma hnot_le_iff_codisjoint_left : ￢a ≤ b ↔ codisjoint b a :=
hnot_le_iff_codisjoint_right.trans codisjoint.comm

lemma hnot_le_comm : ￢a ≤ b ↔ ￢b ≤ a :=
by rw [hnot_le_iff_codisjoint_right, hnot_le_iff_codisjoint_left]

alias hnot_le_iff_codisjoint_right ↔ _ codisjoint.hnot_le_right
alias hnot_le_iff_codisjoint_left ↔ _ codisjoint.hnot_le_left

lemma codisjoint_hnot_right : codisjoint a (￢a) :=
codisjoint_iff_le_sup.2 $ sdiff_le_iff.1 (top_sdiff' _).le
lemma codisjoint_hnot_left : codisjoint (￢a) a := codisjoint_hnot_right.symm

lemma has_le.le.codisjoint_hnot_left (h : a ≤ b) : codisjoint (￢a) b :=
codisjoint_hnot_left.mono_right h

lemma has_le.le.codisjoint_hnot_right (h : b ≤ a) : codisjoint a (￢b) :=
codisjoint_hnot_right.mono_left h

lemma is_compl.hnot_eq (h : is_compl a b) : ￢a = b :=
h.2.hnot_le_right.antisymm $ disjoint.le_of_codisjoint h.1.symm codisjoint_hnot_right

lemma is_compl.eq_hnot (h : is_compl a b) : a = ￢b :=
h.2.hnot_le_left.antisymm' $ disjoint.le_of_codisjoint h.1 codisjoint_hnot_right

@[simp] lemma sup_hnot_self (a : α) : a ⊔ ￢a = ⊤ := codisjoint.eq_top codisjoint_hnot_right
@[simp] lemma hnot_sup_self (a : α) : ￢a ⊔ a = ⊤ := codisjoint.eq_top codisjoint_hnot_left

@[simp] lemma hnot_bot : ￢(⊥ : α) = ⊤ :=
eq_of_forall_ge_iff $ λ a, by rw [hnot_le_iff_codisjoint_left, codisjoint_bot, top_le_iff]

@[simp] lemma hnot_top : ￢(⊤ : α) = ⊥ := by rw [←top_sdiff', sdiff_self]

lemma hnot_hnot_le : ￢￢a ≤ a := codisjoint_hnot_right.hnot_le_left

lemma hnot_anti : antitone (hnot : α → α) := λ a b h, hnot_le_comm.1 $ hnot_hnot_le.trans h

lemma hnot_le_hnot (h : a ≤ b) : ￢b ≤ ￢a := hnot_anti h

@[simp] lemma hnot_hnot_hnot (a : α) : ￢￢￢a = ￢a := hnot_hnot_le.antisymm $ hnot_anti hnot_hnot_le

@[simp] lemma codisjoint_hnot_hnot_left_iff : codisjoint (￢￢a) b ↔ codisjoint a b :=
by simp_rw [←hnot_le_iff_codisjoint_right, hnot_hnot_hnot]

@[simp] lemma codisjoint_hnot_hnot_right_iff : codisjoint a (￢￢b) ↔ codisjoint a b :=
by simp_rw [←hnot_le_iff_codisjoint_left, hnot_hnot_hnot]

lemma le_hnot_inf_hnot : ￢ (a ⊔ b) ≤ ￢a ⊓ ￢b :=
le_inf (hnot_anti le_sup_left) $ hnot_anti le_sup_right

lemma hnot_hnot_sup_distrib (a b : α) : ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b :=
begin
  refine ((hnot_inf_distrib _ _).ge.trans $ hnot_anti le_hnot_inf_hnot).antisymm' _,
  rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff,
    codisjoint_left_comm, codisjoint_hnot_hnot_left_iff, ←codisjoint_assoc, sup_comm],
  exact codisjoint_hnot_right,
end

lemma hnot_hnot_sdiff_distrib (a b : α) : ￢￢(a \ b) = ￢￢a \ ￢￢b :=
begin
  refine le_antisymm _ _,
  { refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' _),
    rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm,
      ←hnot_le_iff_codisjoint_right],
    exact le_sdiff_sup },
  { rw [sdiff_le_iff, ←hnot_hnot_sup_distrib],
    exact hnot_anti (hnot_anti le_sup_sdiff) }
end

instance : heyting_algebra αᵒᵈ :=
{ compl := to_dual ∘ hnot ∘ of_dual,
  himp := λ a b, to_dual (of_dual b \ of_dual a),
  le_himp_iff := λ a b c, by { rw inf_comm, exact sdiff_le_iff },
  himp_bot := top_sdiff',
  ..order_dual.lattice α, ..order_dual.bounded_order α }

@[simp] lemma of_dual_compl (a : αᵒᵈ) : of_dual aᶜ = ￢of_dual a := rfl
@[simp] lemma of_dual_himp (a b : αᵒᵈ) : of_dual (a ⇨ b) = of_dual b \ of_dual a := rfl
@[simp] lemma to_dual_hnot (a : α) : to_dual ￢a = (to_dual a)ᶜ := rfl
@[simp] lemma to_dual_sdiff (a b : α) : to_dual (a \ b) = to_dual b ⇨ to_dual a := rfl

instance prod.coheyting_algebra [coheyting_algebra β] : coheyting_algebra (α × β) :=
{ sdiff_le_iff := λ a b c, and_congr sdiff_le_iff sdiff_le_iff,
  top_sdiff := λ a, prod.ext (top_sdiff' a.1) (top_sdiff' a.2),
  ..prod.lattice α β, ..prod.bounded_order α β, ..prod.has_sdiff, ..prod.has_hnot }

instance pi.coheyting_algebra {α : ι → Type*} [Π i, coheyting_algebra (α i)] :
  coheyting_algebra (Π i, α i) :=
by { pi_instance, exact λ a b c, forall_congr (λ i, sdiff_le_iff) }

end coheyting_algebra

section biheyting_algebra
variables [biheyting_algebra α] {a : α}

lemma compl_le_hnot : aᶜ ≤ ￢a :=
(disjoint_compl_left : disjoint _ a).le_of_codisjoint codisjoint_hnot_right

end biheyting_algebra

/-- Propositions form a Heyting algebra with implication as Heyting implication and negation as
complement. -/
instance Prop.heyting_algebra : heyting_algebra Prop :=
{ himp := (→),
  le_himp_iff := λ p q r, and_imp.symm,
  himp_bot := λ p, rfl,
  ..Prop.has_compl, ..Prop.distrib_lattice, ..Prop.bounded_order }

@[simp] lemma himp_iff_imp (p q : Prop) : p ⇨ q ↔ p → q := iff.rfl
@[simp] lemma compl_iff_not (p : Prop) : pᶜ ↔ ¬ p := iff.rfl

/-- A bounded linear order is a bi-Heyting algebra by setting
* `a ⇨ b = ⊤` if `a ≤ b` and `a ⇨ b = b` otherwise.
* `a \ b = ⊥` if `a ≤ b` and `a \ b = a` otherwise. -/
@[reducible] -- See note [reducible non-instances]
def linear_order.to_biheyting_algebra [linear_order α] [bounded_order α] : biheyting_algebra α :=
{ himp := λ a b, if a ≤ b then ⊤ else b,
  compl := λ a, if a = ⊥ then ⊤ else ⊥,
  le_himp_iff := λ a b c, begin
    change _ ≤ ite _ _ _ ↔ _,
    split_ifs,
    { exact iff_of_true le_top (inf_le_of_right_le h) },
    { rw [inf_le_iff, or_iff_left h] }
  end,
  himp_bot := λ a, if_congr le_bot_iff rfl rfl,
  sdiff := λ a b, if a ≤ b then ⊥ else a,
  hnot := λ a, if a = ⊤ then ⊥ else ⊤,
  sdiff_le_iff := λ a b c, begin
    change ite _ _ _ ≤ _ ↔ _,
    split_ifs,
    { exact iff_of_true bot_le (le_sup_of_le_left h) },
    { rw [le_sup_iff, or_iff_right h] }
  end,
  top_sdiff := λ a, if_congr top_le_iff rfl rfl,
  ..linear_order.to_lattice, ..‹bounded_order α› }

section lift

/-- Pullback a `generalized_heyting_algebra` along an injection. -/
@[reducible] -- See note [reducible non-instances]
protected def function.injective.generalized_heyting_algebra [has_sup α] [has_inf α] [has_top α]
  [has_himp α] [generalized_heyting_algebra β] (f : α → β) (hf : injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_top : f ⊤ = ⊤) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) :
  generalized_heyting_algebra α :=
{ le_top := λ a, by { change f _ ≤ _, rw map_top, exact le_top },
  le_himp_iff := λ a b c, by { change f _ ≤ _ ↔ f _ ≤ _, erw [map_himp, map_inf, le_himp_iff] },
  ..hf.lattice f map_sup map_inf, ..‹has_top α›, ..‹has_himp α› }

/-- Pullback a `generalized_coheyting_algebra` along an injection. -/
@[reducible] -- See note [reducible non-instances]
protected def function.injective.generalized_coheyting_algebra [has_sup α] [has_inf α] [has_bot α]
  [has_sdiff α] [generalized_coheyting_algebra β] (f : α → β) (hf : injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_bot : f ⊥ = ⊥) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  generalized_coheyting_algebra α :=
{ bot_le := λ a, by { change f _ ≤ _, rw map_bot, exact bot_le },
  sdiff_le_iff := λ a b c, by { change f _ ≤ _ ↔ f _ ≤ _, erw [map_sdiff, map_sup, sdiff_le_iff] },
  ..hf.lattice f map_sup map_inf, ..‹has_bot α›, ..‹has_sdiff α› }

/-- Pullback a `heyting_algebra` along an injection. -/
@[reducible] -- See note [reducible non-instances]
protected def function.injective.heyting_algebra [has_sup α] [has_inf α] [has_top α] [has_bot α]
  [has_compl α] [has_himp α] [heyting_algebra β] (f : α → β) (hf : injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_compl : ∀ a, f aᶜ = (f a)ᶜ)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) :
  heyting_algebra α :=
{ bot_le := λ a, by { change f _ ≤ _, rw map_bot, exact bot_le },
  himp_bot := λ a, hf $ by erw [map_himp, map_compl, map_bot, himp_bot],
  ..hf.generalized_heyting_algebra f map_sup map_inf map_top map_himp,
  ..‹has_bot α›, ..‹has_compl α› }

/-- Pullback a `coheyting_algebra` along an injection. -/
@[reducible] -- See note [reducible non-instances]
protected def function.injective.coheyting_algebra [has_sup α] [has_inf α] [has_top α] [has_bot α]
  [has_hnot α] [has_sdiff α] [coheyting_algebra β] (f : α → β) (hf : injective f)
  (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b)
  (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥) (map_hnot : ∀ a, f ￢a = ￢f a)
  (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  coheyting_algebra α :=
{ le_top := λ a, by { change f _ ≤ _, rw map_top, exact le_top },
  top_sdiff := λ a, hf $ by erw [map_sdiff, map_hnot, map_top, top_sdiff'],
  ..hf.generalized_coheyting_algebra f map_sup map_inf map_bot map_sdiff,
  ..‹has_top α›, ..‹has_hnot α› }

/-- Pullback a `biheyting_algebra` along an injection. -/
@[reducible] -- See note [reducible non-instances]
protected def function.injective.biheyting_algebra [has_sup α] [has_inf α] [has_top α] [has_bot α]
  [has_compl α] [has_hnot α] [has_himp α] [has_sdiff α] [biheyting_algebra β] (f : α → β)
  (hf : injective f) (map_sup : ∀ a b, f (a ⊔ b) = f a ⊔ f b)
  (map_inf : ∀ a b, f (a ⊓ b) = f a ⊓ f b) (map_top : f ⊤ = ⊤) (map_bot : f ⊥ = ⊥)
  (map_compl : ∀ a, f aᶜ = (f a)ᶜ) (map_hnot : ∀ a, f ￢a = ￢f a)
  (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) (map_sdiff : ∀ a b, f (a \ b) = f a \ f b) :
  biheyting_algebra α :=
{ ..hf.heyting_algebra f map_sup map_inf map_top map_bot map_compl map_himp,
  ..hf.coheyting_algebra f map_sup map_inf map_top map_bot map_hnot map_sdiff }

end lift

namespace punit
variables (a b : punit.{u+1})

instance : biheyting_algebra punit :=
by refine_struct
{ top := star,
  bot := star,
  sup := λ _ _, star,
  inf := λ _ _, star,
  compl := λ _, star,
  sdiff := λ _ _, star,
  hnot := λ _, star,
  himp := λ _ _, star, ..punit.linear_order };
    intros; trivial <|> exact subsingleton.elim _ _

@[simp] lemma top_eq : (⊤ : punit) = star := rfl
@[simp] lemma bot_eq : (⊥ : punit) = star := rfl
@[simp] lemma sup_eq : a ⊔ b = star := rfl
@[simp] lemma inf_eq : a ⊓ b = star := rfl
@[simp] lemma compl_eq : aᶜ = star := rfl
@[simp] lemma sdiff_eq : a \ b = star := rfl
@[simp, nolint simp_nf] lemma hnot_eq : ￢a = star := rfl -- eligible for `dsimp`
@[simp] lemma himp_eq : a ⇨ b = star := rfl

end punit

repo: mathlib


text:
/-
Copyright (c) 2020 Joseph Myers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Myers, Yury Kudryashov
-/
import analysis.normed.group.basic
import linear_algebra.affine_space.midpoint

/-!
# Torsors of additive normed group actions.

This file defines torsors of additive normed group actions, with a
metric space structure.  The motivating case is Euclidean affine
spaces.
-/

noncomputable theory
open_locale nnreal topological_space
open filter

/-- A `normed_add_torsor V P` is a torsor of an additive seminormed group
action by a `semi_normed_group V` on points `P`. We bundle the pseudometric space
structure and require the distance to be the same as results from the
norm (which in fact implies the distance yields a pseudometric space, but
bundling just the distance and using an instance for the pseudometric space
results in type class problems). -/
class normed_add_torsor (V : out_param $ Type*) (P : Type*)
  [out_param $ semi_normed_group V] [pseudo_metric_space P]
  extends add_torsor V P :=
(dist_eq_norm' : ∀ (x y : P), dist x y = ∥(x -ᵥ y : V)∥)

variables {α V P : Type*} [semi_normed_group V] [pseudo_metric_space P] [normed_add_torsor V P]
variables {W Q : Type*} [normed_group W] [metric_space Q] [normed_add_torsor W Q]

/-- A `semi_normed_group` is a `normed_add_torsor` over itself. -/
@[priority 100]
instance semi_normed_group.to_normed_add_torsor : normed_add_torsor V V :=
{ dist_eq_norm' := dist_eq_norm }

include V

section

variables (V W)

/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub` sometimes doesn't work. -/
lemma dist_eq_norm_vsub (x y : P) : dist x y = ∥x -ᵥ y∥ := normed_add_torsor.dist_eq_norm' x y

/-- The distance equals the norm of subtracting two points. In this
lemma, it is necessary to have `V` as an explicit argument; otherwise
`rw dist_eq_norm_vsub'` sometimes doesn't work. -/
lemma dist_eq_norm_vsub' (x y : P) : dist x y = ∥y -ᵥ x∥ :=
(dist_comm _ _).trans (dist_eq_norm_vsub _ _ _)

end

@[simp] lemma dist_vadd_cancel_left (v : V) (x y : P) :
  dist (v +ᵥ x) (v +ᵥ y) = dist x y :=
by rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, vadd_vsub_vadd_cancel_left]

@[simp] lemma dist_vadd_cancel_right (v₁ v₂ : V) (x : P) :
  dist (v₁ +ᵥ x) (v₂ +ᵥ x) = dist v₁ v₂ :=
by rw [dist_eq_norm_vsub V, dist_eq_norm, vadd_vsub_vadd_cancel_right]

@[simp] lemma dist_vadd_left (v : V) (x : P) : dist (v +ᵥ x) x = ∥v∥ :=
by simp [dist_eq_norm_vsub V _ x]

@[simp] lemma dist_vadd_right (v : V) (x : P) : dist x (v +ᵥ x) = ∥v∥ :=
by rw [dist_comm, dist_vadd_left]

/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
addition/subtraction of `x : P`. -/
@[simps] def isometric.vadd_const (x : P) : V ≃ᵢ P :=
{ to_equiv := equiv.vadd_const x,
  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_right _ _ _ }

section

variable (P)

/-- Self-isometry of a (semi)normed add torsor given by addition of a constant vector `x`. -/
@[simps] def isometric.const_vadd (x : V) : P ≃ᵢ P :=
{ to_equiv := equiv.const_vadd P x,
  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ _ _, dist_vadd_cancel_left _ _ _ }

end

@[simp] lemma dist_vsub_cancel_left (x y z : P) : dist (x -ᵥ y) (x -ᵥ z) = dist y z :=
by rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]

/-- Isometry between the tangent space `V` of a (semi)normed add torsor `P` and `P` given by
subtraction from `x : P`. -/
@[simps] def isometric.const_vsub (x : P) : P ≃ᵢ V :=
{ to_equiv := equiv.const_vsub x,
  isometry_to_fun := isometry_emetric_iff_metric.2 $ λ y z, dist_vsub_cancel_left _ _ _ }

@[simp] lemma dist_vsub_cancel_right (x y z : P) : dist (x -ᵥ z) (y -ᵥ z) = dist x y :=
(isometric.vadd_const z).symm.dist_eq x y

section pointwise

open_locale pointwise

@[simp] lemma vadd_ball (x : V) (y : P) (r : ℝ) :
  x +ᵥ metric.ball y r = metric.ball (x +ᵥ y) r :=
(isometric.const_vadd P x).image_ball y r

@[simp] lemma vadd_closed_ball (x : V) (y : P) (r : ℝ) :
  x +ᵥ metric.closed_ball y r = metric.closed_ball (x +ᵥ y) r :=
(isometric.const_vadd P x).image_closed_ball y r

@[simp] lemma vadd_sphere (x : V) (y : P) (r : ℝ) :
  x +ᵥ metric.sphere y r = metric.sphere (x +ᵥ y) r :=
(isometric.const_vadd P x).image_sphere y r

end pointwise

lemma dist_vadd_vadd_le (v v' : V) (p p' : P) :
  dist (v +ᵥ p) (v' +ᵥ p') ≤ dist v v' + dist p p' :=
by simpa using dist_triangle (v +ᵥ p) (v' +ᵥ p) (v' +ᵥ p')

lemma dist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
  dist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ dist p₁ p₃ + dist p₂ p₄ :=
by { rw [dist_eq_norm, vsub_sub_vsub_comm, dist_eq_norm_vsub V, dist_eq_norm_vsub V],
 exact norm_sub_le _ _ }

lemma nndist_vadd_vadd_le (v v' : V) (p p' : P) :
  nndist (v +ᵥ p) (v' +ᵥ p') ≤ nndist v v' + nndist p p' :=
by simp only [← nnreal.coe_le_coe, nnreal.coe_add, ← dist_nndist, dist_vadd_vadd_le]

lemma nndist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
  nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄ :=
by simp only [← nnreal.coe_le_coe, nnreal.coe_add, ← dist_nndist, dist_vsub_vsub_le]

lemma edist_vadd_vadd_le (v v' : V) (p p' : P) :
  edist (v +ᵥ p) (v' +ᵥ p') ≤ edist v v' + edist p p' :=
by { simp only [edist_nndist], apply_mod_cast nndist_vadd_vadd_le }

lemma edist_vsub_vsub_le (p₁ p₂ p₃ p₄ : P) :
  edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄ :=
by { simp only [edist_nndist], apply_mod_cast nndist_vsub_vsub_le }

omit V

/-- The pseudodistance defines a pseudometric space structure on the torsor. This
is not an instance because it depends on `V` to define a `metric_space
P`. -/
def pseudo_metric_space_of_normed_group_of_add_torsor (V P : Type*) [semi_normed_group V]
  [add_torsor V P] : pseudo_metric_space P :=
{ dist := λ x y, ∥(x -ᵥ y : V)∥,
  dist_self := λ x, by simp,
  dist_comm := λ x y, by simp only [←neg_vsub_eq_vsub_rev y x, norm_neg],
  dist_triangle := begin
    intros x y z,
    change ∥x -ᵥ z∥ ≤ ∥x -ᵥ y∥ + ∥y -ᵥ z∥,
    rw ←vsub_add_vsub_cancel,
    apply norm_add_le
  end }

/-- The distance defines a metric space structure on the torsor. This
is not an instance because it depends on `V` to define a `metric_space
P`. -/
def metric_space_of_normed_group_of_add_torsor (V P : Type*) [normed_group V] [add_torsor V P] :
  metric_space P :=
{ dist := λ x y, ∥(x -ᵥ y : V)∥,
  dist_self := λ x, by simp,
  eq_of_dist_eq_zero := λ x y h, by simpa using h,
  dist_comm := λ x y, by simp only [←neg_vsub_eq_vsub_rev y x, norm_neg],
  dist_triangle := begin
    intros x y z,
    change ∥x -ᵥ z∥ ≤ ∥x -ᵥ y∥ + ∥y -ᵥ z∥,
    rw ←vsub_add_vsub_cancel,
    apply norm_add_le
  end }

include V

lemma lipschitz_with.vadd [pseudo_emetric_space α] {f : α → V} {g : α → P} {Kf Kg : ℝ≥0}
  (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
  lipschitz_with (Kf + Kg) (f +ᵥ g) :=
λ x y,
calc edist (f x +ᵥ g x) (f y +ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :
  edist_vadd_vadd_le _ _ _ _
... ≤ Kf * edist x y + Kg * edist x y :
  add_le_add (hf x y) (hg x y)
... = (Kf + Kg) * edist x y :
  (add_mul _ _ _).symm

lemma lipschitz_with.vsub [pseudo_emetric_space α] {f g : α → P} {Kf Kg : ℝ≥0}
  (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :
  lipschitz_with (Kf + Kg) (f -ᵥ g) :=
λ x y,
calc edist (f x -ᵥ g x) (f y -ᵥ g y) ≤ edist (f x) (f y) + edist (g x) (g y) :
  edist_vsub_vsub_le _ _ _ _
... ≤ Kf * edist x y + Kg * edist x y :
  add_le_add (hf x y) (hg x y)
... = (Kf + Kg) * edist x y :
  (add_mul _ _ _).symm

lemma uniform_continuous_vadd : uniform_continuous (λ x : V × P, x.1 +ᵥ x.2) :=
(lipschitz_with.prod_fst.vadd lipschitz_with.prod_snd).uniform_continuous

lemma uniform_continuous_vsub : uniform_continuous (λ x : P × P, x.1 -ᵥ x.2) :=
(lipschitz_with.prod_fst.vsub lipschitz_with.prod_snd).uniform_continuous

@[priority 100] instance normed_add_torsor.to_has_continuous_vadd : has_continuous_vadd V P :=
{ continuous_vadd := uniform_continuous_vadd.continuous }

lemma continuous_vsub : continuous (λ x : P × P, x.1 -ᵥ x.2) :=
uniform_continuous_vsub.continuous

lemma filter.tendsto.vsub {l : filter α} {f g : α → P} {x y : P}
  (hf : tendsto f l (𝓝 x)) (hg : tendsto g l (𝓝 y)) :
  tendsto (f -ᵥ g) l (𝓝 (x -ᵥ y)) :=
(continuous_vsub.tendsto (x, y)).comp (hf.prod_mk_nhds hg)

section

variables [topological_space α]

lemma continuous.vsub {f g : α → P} (hf : continuous f) (hg : continuous g) :
  continuous (f -ᵥ g) :=
continuous_vsub.comp (hf.prod_mk hg : _)

lemma continuous_at.vsub {f g : α → P}  {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
  continuous_at (f -ᵥ g) x :=
hf.vsub hg

lemma continuous_within_at.vsub {f g : α → P} {x : α} {s : set α}
  (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
  continuous_within_at (f -ᵥ g) s x :=
hf.vsub hg

end

section

variables {R : Type*} [ring R] [topological_space R] [module R V] [has_continuous_smul R V]

lemma filter.tendsto.line_map {l : filter α} {f₁ f₂ : α → P} {g : α → R} {p₁ p₂ : P} {c : R}
  (h₁ : tendsto f₁ l (𝓝 p₁)) (h₂ : tendsto f₂ l (𝓝 p₂)) (hg : tendsto g l (𝓝 c)) :
  tendsto (λ x, affine_map.line_map (f₁ x) (f₂ x) (g x)) l (𝓝 $ affine_map.line_map p₁ p₂ c) :=
(hg.smul (h₂.vsub h₁)).vadd h₁

lemma filter.tendsto.midpoint [invertible (2:R)] {l : filter α} {f₁ f₂ : α → P} {p₁ p₂ : P}
  (h₁ : tendsto f₁ l (𝓝 p₁)) (h₂ : tendsto f₂ l (𝓝 p₂)) :
  tendsto (λ x, midpoint R (f₁ x) (f₂ x)) l (𝓝 $ midpoint R p₁ p₂) :=
h₁.line_map h₂ tendsto_const_nhds

end

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools


text:
/-
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta

! This file was ported from Lean 3 source module category_theory.subterminal
! leanprover-community/mathlib commit bb103f356534a9a7d3596a672097e375290a4c3a
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathbin.CategoryTheory.Limits.Shapes.Terminal
import Mathbin.CategoryTheory.Subobject.MonoOver

/-!
# Subterminal objects

Subterminal objects are the objects which can be thought of as subobjects of the terminal object.
In fact, the definition can be constructed to not require a terminal object, by defining `A` to be
subterminal iff for any `Z`, there is at most one morphism `Z ⟶ A`.
An alternate definition is that the diagonal morphism `A ⟶ A ⨯ A` is an isomorphism.
In this file we define subterminal objects and show the equivalence of these three definitions.

We also construct the subcategory of subterminal objects.

## TODO

* Define exponential ideals, and show this subcategory is an exponential ideal.
* Use the above to show that in a locally cartesian closed category, every subobject lattice
  is cartesian closed (equivalently, a Heyting algebra).

-/

universe v₁ v₂ u₁ u₂

noncomputable section

namespace CategoryTheory

open Limits Category

variable {C : Type u₁} [Category.{v₁} C] {A : C}

/-- An object `A` is subterminal iff for any `Z`, there is at most one morphism `Z ⟶ A`. -/
def IsSubterminal (A : C) : Prop :=
  ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
#align category_theory.is_subterminal CategoryTheory.IsSubterminal

theorem IsSubterminal.def : IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g :=
  Iff.rfl
#align category_theory.is_subterminal.def CategoryTheory.IsSubterminal.def

/-- If `A` is subterminal, the unique morphism from it to a terminal object is a monomorphism.
The converse of `is_subterminal_of_mono_is_terminal_from`.
-/
theorem IsSubterminal.mono_isTerminal_from (hA : IsSubterminal A) {T : C} (hT : IsTerminal T) :
    Mono (hT.from A) :=
  { right_cancellation := fun Z g h _ => hA _ _ }
#align category_theory.is_subterminal.mono_is_terminal_from CategoryTheory.IsSubterminal.mono_isTerminal_from

/-- If `A` is subterminal, the unique morphism from it to the terminal object is a monomorphism.
The converse of `is_subterminal_of_mono_terminal_from`.
-/
theorem IsSubterminal.mono_terminal_from [HasTerminal C] (hA : IsSubterminal A) :
    Mono (terminal.from A) :=
  hA.mono_isTerminal_from terminalIsTerminal
#align category_theory.is_subterminal.mono_terminal_from CategoryTheory.IsSubterminal.mono_terminal_from

/-- If the unique morphism from `A` to a terminal object is a monomorphism, `A` is subterminal.
The converse of `is_subterminal.mono_is_terminal_from`.
-/
theorem isSubterminal_of_mono_isTerminal_from {T : C} (hT : IsTerminal T) [Mono (hT.from A)] :
    IsSubterminal A := fun Z f g =>
  by
  rw [← cancel_mono (hT.from A)]
  apply hT.hom_ext
#align category_theory.is_subterminal_of_mono_is_terminal_from CategoryTheory.isSubterminal_of_mono_isTerminal_from

/-- If the unique morphism from `A` to the terminal object is a monomorphism, `A` is subterminal.
The converse of `is_subterminal.mono_terminal_from`.
-/
theorem isSubterminal_of_mono_terminal_from [HasTerminal C] [Mono (terminal.from A)] :
    IsSubterminal A := fun Z f g =>
  by
  rw [← cancel_mono (terminal.from A)]
  apply Subsingleton.elim
#align category_theory.is_subterminal_of_mono_terminal_from CategoryTheory.isSubterminal_of_mono_terminal_from

theorem isSubterminal_of_isTerminal {T : C} (hT : IsTerminal T) : IsSubterminal T := fun Z f g =>
  hT.hom_ext _ _
#align category_theory.is_subterminal_of_is_terminal CategoryTheory.isSubterminal_of_isTerminal

theorem isSubterminal_of_terminal [HasTerminal C] : IsSubterminal (⊤_ C) := fun Z f g =>
  Subsingleton.elim _ _
#align category_theory.is_subterminal_of_terminal CategoryTheory.isSubterminal_of_terminal

/-- If `A` is subterminal, its diagonal morphism is an isomorphism.
The converse of `is_subterminal_of_is_iso_diag`.
-/
theorem IsSubterminal.isIso_diag (hA : IsSubterminal A) [HasBinaryProduct A A] : IsIso (diag A) :=
  ⟨⟨Limits.prod.fst,
      ⟨by simp, by
        rw [is_subterminal.def] at hA
        tidy⟩⟩⟩
#align category_theory.is_subterminal.is_iso_diag CategoryTheory.IsSubterminal.isIso_diag

/-- If the diagonal morphism of `A` is an isomorphism, then it is subterminal.
The converse of `is_subterminal.is_iso_diag`.
-/
theorem isSubterminal_of_isIso_diag [HasBinaryProduct A A] [IsIso (diag A)] : IsSubterminal A :=
  fun Z f g =>
  by
  have : (limits.prod.fst : A ⨯ A ⟶ _) = limits.prod.snd := by simp [← cancel_epi (diag A)]
  rw [← prod.lift_fst f g, this, prod.lift_snd]
#align category_theory.is_subterminal_of_is_iso_diag CategoryTheory.isSubterminal_of_isIso_diag

/-- If `A` is subterminal, it is isomorphic to `A ⨯ A`. -/
@[simps]
def IsSubterminal.isoDiag (hA : IsSubterminal A) [HasBinaryProduct A A] : A ⨯ A ≅ A :=
  by
  letI := is_subterminal.is_iso_diag hA
  apply (as_iso (diag A)).symm
#align category_theory.is_subterminal.iso_diag CategoryTheory.IsSubterminal.isoDiag

variable (C)

/-- The (full sub)category of subterminal objects.
TODO: If `C` is the category of sheaves on a topological space `X`, this category is equivalent
to the lattice of open subsets of `X`. More generally, if `C` is a topos, this is the lattice of
"external truth values".
-/
def Subterminals (C : Type u₁) [Category.{v₁} C] :=
  FullSubcategory fun A : C => IsSubterminal A deriving Category
#align category_theory.subterminals CategoryTheory.Subterminals

instance [HasTerminal C] : Inhabited (Subterminals C) :=
  ⟨⟨⊤_ C, isSubterminal_of_terminal⟩⟩

/-- The inclusion of the subterminal objects into the original category. -/
@[simps]
def subterminalInclusion : Subterminals C ⥤ C :=
  fullSubcategoryInclusion _ deriving Full, Faithful
#align category_theory.subterminal_inclusion CategoryTheory.subterminalInclusion

instance subterminals_thin (X Y : Subterminals C) : Subsingleton (X ⟶ Y) :=
  ⟨fun f g => Y.2 f g⟩
#align category_theory.subterminals_thin CategoryTheory.subterminals_thin

/--
The category of subterminal objects is equivalent to the category of monomorphisms to the terminal
object (which is in turn equivalent to the subobjects of the terminal object).
-/
@[simps]
def subterminalsEquivMonoOverTerminal [HasTerminal C] : Subterminals C ≌ MonoOver (⊤_ C)
    where
  Functor :=
    { obj := fun X => ⟨Over.mk (terminal.from X.1), X.2.mono_terminal_from⟩
      map := fun X Y f => MonoOver.homMk f (by ext1 ⟨⟨⟩⟩) }
  inverse :=
    { obj := fun X =>
        ⟨X.obj.left, fun Z f g => by
          rw [← cancel_mono X.arrow]
          apply Subsingleton.elim⟩
      map := fun X Y f => f.1 }
  unitIso :=
    { Hom := { app := fun X => 𝟙 _ }
      inv := { app := fun X => 𝟙 _ } }
  counitIso :=
    { Hom := { app := fun X => Over.homMk (𝟙 _) }
      inv := { app := fun X => Over.homMk (𝟙 _) } }
#align category_theory.subterminals_equiv_mono_over_terminal CategoryTheory.subterminalsEquivMonoOverTerminal

@[simp]
theorem subterminals_to_monoOver_terminal_comp_forget [HasTerminal C] :
    (subterminalsEquivMonoOverTerminal C).Functor ⋙ MonoOver.forget _ ⋙ Over.forget _ =
      subterminalInclusion C :=
  rfl
#align category_theory.subterminals_to_mono_over_terminal_comp_forget CategoryTheory.subterminals_to_monoOver_terminal_comp_forget

@[simp]
theorem monoOver_terminal_to_subterminals_comp [HasTerminal C] :
    (subterminalsEquivMonoOverTerminal C).inverse ⋙ subterminalInclusion C =
      MonoOver.forget _ ⋙ Over.forget _ :=
  rfl
#align category_theory.mono_over_terminal_to_subterminals_comp CategoryTheory.monoOver_terminal_to_subterminals_comp

end CategoryTheory

author: leanprover-community


text:
/-
Copyright (c) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.finset.fold
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.Monoid.WithTop
import Mathlib.Data.Finset.Image
import Mathlib.Data.Multiset.Fold

/-!
# The fold operation for a commutative associative operation over a finset.
-/

namespace Finset

open Multiset

variable {α β γ : Type _}

/-! ### fold -/

section Fold

variable (op : β → β → β) [hc : IsCommutative β op] [ha : IsAssociative β op]

local notation a " * " b => op a b

/-- `fold op b f s` folds the commutative associative operation `op` over the
  `f`-image of `s`, i.e. `fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b`. -/
def fold (b : β) (f : α → β) (s : Finset α) : β :=
  (s.1.map f).fold op b
#align finset.fold Finset.fold

variable {op} {f : α → β} {b : β} {s : Finset α} {a : α}

@[simp]
theorem fold_empty : (∅ : Finset α).fold op b f = b :=
  rfl
#align finset.fold_empty Finset.fold_empty

@[simp]
theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f := by
  dsimp only [fold]
  rw [cons_val, Multiset.map_cons, fold_cons_left]
#align finset.fold_cons Finset.fold_cons

@[simp]
theorem fold_insert [DecidableEq α] (h : a ∉ s) :
    (insert a s).fold op b f = f a * s.fold op b f := by
  unfold fold
  rw [insert_val, ndinsert_of_not_mem h, Multiset.map_cons, fold_cons_left]
#align finset.fold_insert Finset.fold_insert

@[simp]
theorem fold_singleton : ({a} : Finset α).fold op b f = f a * b :=
  rfl
#align finset.fold_singleton Finset.fold_singleton

@[simp]
theorem fold_map {g : γ ↪ α} {s : Finset γ} : (s.map g).fold op b f = s.fold op b (f ∘ g) := by
  simp only [fold, map, Multiset.map_map]
#align finset.fold_map Finset.fold_map

@[simp]
theorem fold_image [DecidableEq α] {g : γ → α} {s : Finset γ}
    (H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g) := by
  simp only [fold, image_val_of_injOn H, Multiset.map_map]
#align finset.fold_image Finset.fold_image

@[congr]
theorem fold_congr {g : α → β} (H : ∀ x ∈ s, f x = g x) : s.fold op b f = s.fold op b g := by
  rw [fold, fold, map_congr rfl H]
#align finset.fold_congr Finset.fold_congr

theorem fold_op_distrib {f g : α → β} {b₁ b₂ : β} :
    (s.fold op (b₁ * b₂) fun x => f x * g x) = s.fold op b₁ f * s.fold op b₂ g := by
  simp only [fold, fold_distrib]
#align finset.fold_op_distrib Finset.fold_op_distrib

theorem fold_const [hd : Decidable (s = ∅)] (c : β) (h : op c (op b c) = op b c) :
    Finset.fold op b (fun _ => c) s = if s = ∅ then b else op b c := by
  classical
    induction' s using Finset.induction_on with x s hx IH generalizing hd
    · simp
    · simp only [Finset.fold_insert hx, IH, if_false, Finset.insert_ne_empty]
      split_ifs
      · rw [hc.comm]
      · exact h
#align finset.fold_const Finset.fold_const

theorem fold_hom {op' : γ → γ → γ} [IsCommutative γ op'] [IsAssociative γ op'] {m : β → γ}
    (hm : ∀ x y, m (op x y) = op' (m x) (m y)) :
    (s.fold op' (m b) fun x => m (f x)) = m (s.fold op b f) := by
  rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]
  simp only [Function.comp_apply]
#align finset.fold_hom Finset.fold_hom

theorem fold_disjUnion {s₁ s₂ : Finset α} {b₁ b₂ : β} (h) :
    (s₁.disjUnion s₂ h).fold op (b₁ * b₂) f = s₁.fold op b₁ f * s₂.fold op b₂ f :=
  (congr_arg _ <| Multiset.map_add _ _ _).trans (Multiset.fold_add _ _ _ _ _)
#align finset.fold_disj_union Finset.fold_disjUnion

theorem fold_disjUnionᵢ {ι : Type _} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h) :
    (s.disjUnionᵢ t h).fold op (s.fold op b₀ b) f = s.fold op b₀ fun i => (t i).fold op (b i) f :=
  (congr_arg _ <| Multiset.map_bind _ _ _).trans (Multiset.fold_bind _ _ _ _ _)
#align finset.fold_disj_Union Finset.fold_disjUnionᵢ

theorem fold_union_inter [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β} :
    ((s₁ ∪ s₂).fold op b₁ f * (s₁ ∩ s₂).fold op b₂ f) = s₁.fold op b₂ f * s₂.fold op b₁ f := by
  unfold fold
  rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
    hc.comm, fold_add]
#align finset.fold_union_inter Finset.fold_union_inter

@[simp]
theorem fold_insert_idem [DecidableEq α] [hi : IsIdempotent β op] :
    (insert a s).fold op b f = f a * s.fold op b f := by
  by_cases h : a ∈ s
  · rw [← insert_erase h]
    simp [← ha.assoc, hi.idempotent]
  · apply fold_insert h
#align finset.fold_insert_idem Finset.fold_insert_idem

theorem fold_image_idem [DecidableEq α] {g : γ → α} {s : Finset γ} [hi : IsIdempotent β op] :
    (image g s).fold op b f = s.fold op b (f ∘ g) := by
  induction' s using Finset.cons_induction with x xs hx ih
  · rw [fold_empty, image_empty, fold_empty]
  · haveI := Classical.decEq γ
    rw [fold_cons, cons_eq_insert, image_insert, fold_insert_idem, ih]
    simp only [Function.comp_apply]
#align finset.fold_image_idem Finset.fold_image_idem

/-- A stronger version of `Finset.fold_ite`, but relies on
an explicit proof of idempotency on the seed element, rather
than relying on typeclass idempotency over the whole type. -/
theorem fold_ite' {g : α → β} (hb : op b b = b) (p : α → Prop) [DecidablePred p] :
    Finset.fold op b (fun i => ite (p i) (f i) (g i)) s =
      op (Finset.fold op b f (s.filter p)) (Finset.fold op b g (s.filter fun i => ¬p i)) := by
  classical
    induction' s using Finset.induction_on with x s hx IH
    · simp [hb]
    · simp only [Finset.fold_insert hx]
      split_ifs with h
      · have : x ∉ Finset.filter p s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, ha.assoc, IH]
      · have : x ∉ Finset.filter (fun i => ¬ p i) s := by simp [hx]
        simp [Finset.filter_insert, h, Finset.fold_insert this, IH, ← ha.assoc, hc.comm]
#align finset.fold_ite' Finset.fold_ite'

/-- A weaker version of `Finset.fold_ite'`,
relying on typeclass idempotency over the whole type,
instead of solely on the seed element.
However, this is easier to use because it does not generate side goals. -/
theorem fold_ite [IsIdempotent β op] {g : α → β} (p : α → Prop) [DecidablePred p] :
    Finset.fold op b (fun i => ite (p i) (f i) (g i)) s =
      op (Finset.fold op b f (s.filter p)) (Finset.fold op b g (s.filter fun i => ¬p i)) :=
  fold_ite' (IsIdempotent.idempotent _) _
#align finset.fold_ite Finset.fold_ite

theorem fold_op_rel_iff_and {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∧ r x z)
    {c : β} : r c (s.fold op b f) ↔ r c b ∧ ∀ x ∈ s, r c (f x) := by
  classical
    induction' s using Finset.induction_on with a s ha IH
    · simp
    rw [Finset.fold_insert ha, hr, IH, ← and_assoc, @and_comm (r c (f a)), and_assoc]
    apply and_congr Iff.rfl
    constructor
    · rintro ⟨h₁, h₂⟩
      intro b hb
      rw [Finset.mem_insert] at hb
      rcases hb with (rfl | hb) <;> solve_by_elim
    · intro h
      constructor
      · exact h a (Finset.mem_insert_self _ _)
      · exact fun b hb => h b <| Finset.mem_insert_of_mem hb
#align finset.fold_op_rel_iff_and Finset.fold_op_rel_iff_and

theorem fold_op_rel_iff_or {r : β → β → Prop} (hr : ∀ {x y z}, r x (op y z) ↔ r x y ∨ r x z)
    {c : β} : r c (s.fold op b f) ↔ r c b ∨ ∃ x ∈ s, r c (f x) := by
  classical
    induction' s using Finset.induction_on with a s ha IH
    · simp
    rw [Finset.fold_insert ha, hr, IH, ← or_assoc, @or_comm (r c (f a)), or_assoc]
    apply or_congr Iff.rfl
    constructor
    · rintro (h₁ | ⟨x, hx, h₂⟩)
      · use a
        simp [h₁]
      · refine' ⟨x, by simp [hx], h₂⟩
    · rintro ⟨x, hx, h⟩
      exact (mem_insert.mp hx).imp (fun hx => by rwa [hx] at h) (fun hx => ⟨x, hx, h⟩)
#align finset.fold_op_rel_iff_or Finset.fold_op_rel_iff_or

@[simp]
theorem fold_union_empty_singleton [DecidableEq α] (s : Finset α) :
    Finset.fold (· ∪ ·) ∅ singleton s = s := by
  induction' s using Finset.induction_on with a s has ih
  · simp only [fold_empty]
  · rw [fold_insert has, ih, insert_eq]
#align finset.fold_union_empty_singleton Finset.fold_union_empty_singleton

theorem fold_sup_bot_singleton [DecidableEq α] (s : Finset α) :
    Finset.fold (· ⊔ ·) ⊥ singleton s = s :=
  fold_union_empty_singleton s
#align finset.fold_sup_bot_singleton Finset.fold_sup_bot_singleton

section Order

variable [LinearOrder β] (c : β)

theorem le_fold_min : c ≤ s.fold min b f ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x :=
  fold_op_rel_iff_and le_min_iff
#align finset.le_fold_min Finset.le_fold_min

theorem fold_min_le : s.fold min b f ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c := by
  show _ ≥ _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  show _ ≤ _ ↔ _
  exact min_le_iff
#align finset.fold_min_le Finset.fold_min_le

theorem lt_fold_min : c < s.fold min b f ↔ c < b ∧ ∀ x ∈ s, c < f x :=
  fold_op_rel_iff_and lt_min_iff
#align finset.lt_fold_min Finset.lt_fold_min

theorem fold_min_lt : s.fold min b f < c ↔ b < c ∨ ∃ x ∈ s, f x < c := by
  show _ > _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  show _ < _ ↔ _
  exact min_lt_iff
#align finset.fold_min_lt Finset.fold_min_lt

theorem fold_max_le : s.fold max b f ≤ c ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c := by
  show _ ≥ _ ↔ _
  apply fold_op_rel_iff_and
  intro x y z
  show _ ≤ _ ↔ _
  exact max_le_iff
#align finset.fold_max_le Finset.fold_max_le

theorem le_fold_max : c ≤ s.fold max b f ↔ c ≤ b ∨ ∃ x ∈ s, c ≤ f x :=
  fold_op_rel_iff_or le_max_iff
#align finset.le_fold_max Finset.le_fold_max

theorem lt_fold_max : c < s.fold max b f ↔ c < b ∨ ∃ x ∈ s, c < f x :=
  fold_op_rel_iff_or lt_max_iff
#align finset.lt_fold_max Finset.lt_fold_max

theorem fold_max_add [Add β] [CovariantClass β β (Function.swap (· + ·)) (· ≤ ·)] (n : WithBot β)
    (s : Finset α) : (s.fold max ⊥ fun x : α => ↑(f x) + n) = s.fold max ⊥ ((↑) ∘ f) + n := by
  classical
    induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]
#align finset.fold_max_add Finset.fold_max_add

end Order

end Fold

end Finset


text:
import game.limits.Blockus_Time
import game.sets.L01defs
import game.sup_inf.GLBprop_if_LUBprop
import game.limits.bounded_if_convergent
import game.limits.Lemmas
import data.real.basic
import tactic.linarith

namespace xena

local notation `|`x`|` := abs x

def ev_bdd_away_zero (a : ℕ → ℝ)  := ∃c : ℝ, (0 < c) ∧ (∃ N : ℕ, ∀ n : ℕ, N ≤ n → (c ≤ |a n|))

lemma lim_nz_ev_bdd_away_zero (b : ℕ → ℝ) {k : ℝ} (hk : k ≠ 0) : is_limit b k → ev_bdd_away_zero b :=
begin
  intro j,
  unfold ev_bdd_away_zero,

  unfold is_limit at j,
  use |k| / 2,
  split,
  have T := abs_pos_of_ne_zero hk,
  linarith,

  use 0,
  intro n,
  intro y,
  have Y : |b n| - |k| ≤ |b n - k|,
  exact abs_sub_abs_le_abs_sub _ _,
  have R : 0 ≤ |b n - k|,
  exact abs_nonneg _,
  have P : | |b n| - |k| | < |k| / 2,

  have O : |k| - |k| / 2 < |b n|,

  /-
  intro p,
  have Q := j(|k| / 2) p,
  cases Q with n hd,
  use n,
  intro n,
  intro y,
  have M := hd(n) y,
  have L : | |b n| - |k| | ≤ |b n - k|,
  exact abs_abs_sub_abs_le_abs_sub _ _,
  have P : | |b n| - |k| | < |k| / 2,
  linarith,
  rw abs_lt at P,
  cases P with d hd,
  have O : |k| - |k| / 2 < |b n|,
  linarith,
  have R : |k| - |k| / 2 = |k| / 2,
  ring,
  rw R at O,
  apply lt_imp_le,
  exact O,
  -/
end

/-
have Y : |b n| - |k| ≤ |b n - k|,
  exact abs_sub_abs_le_abs_sub _ _,
  have R : 0 ≤ |b n - k|,
  exact abs_nonneg _,
  --rw abs_abs_sub_abs_le_abs_sub
  norm_num,
  have O : |b n| ≤ |b n - k| + |k|,
  linarith,
  have U : |k| ≤ |b n - k| + |k| + |b n - k| → |k| ≤ |b n| + |b n - k|,
  intro B,
-/

end xena -- hide

author: DavidTalone

repo: Real-Number-Game